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:24;
then prob (A \/ (A `)) = (prob A) + (prob (A `)) by Th21;
then prob ([#] E) = (prob A) + (prob (A `)) by SUBSET_1:10;
then 1 = (prob A) + (prob (A `)) by XCMPLX_1:60;
hence ( prob A = 1 - (prob (A `)) & prob (A `) = 1 - (prob A) ) ; :: thesis: verum