let E be non empty finite set ; :: thesis: for A being Event of E holds
( prob A = 1 - (prob (A ` )) & prob (A ` ) = 1 - (prob A) )
let A be Event of E; :: thesis: ( prob A = 1 - (prob (A ` )) & prob (A ` ) = 1 - (prob A) )
A misses A ` by SUBSET_1:44;
then prob (A \/ (A ` )) = (prob A) + (prob (A ` )) by Th47;
then prob ([#] E) = (prob A) + (prob (A ` )) by SUBSET_1:25;
then 1 = (prob A) + (prob (A ` )) by Th39;
hence ( prob A = 1 - (prob (A ` )) & prob (A ` ) = 1 - (prob A) ) ; :: thesis: verum