let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let P be Probability of Sigma; :: thesis: for A being set holds
( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
let A be set ; :: thesis: ( A in COM (Sigma,P) iff ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) )
thus ( A in COM (Sigma,P) implies ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ) :: thesis: ( ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) )

proof

assume A in COM (Sigma,P) ; :: thesis: ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 )
then consider B being set such that
A1: B in Sigma and
A2: ex C being thin of P st A = B \/ C by Def5;
consider C being thin of P such that
A3: A = B \/ C by A2;
reconsider B = B as Event of Sigma by A1;
consider D being set such that
A4: D in Sigma and
A5: C c= D and
A6: P . D = 0 by Def4;
reconsider D = D as Event of Sigma by A4;
reconsider E = D \/ B as Event of Sigma ;
A7: P . (D \/ B) <= (P . D) + (P . B) by PROB_1:39;
P . (E \ B) = P . (D \ B) by XBOOLE_1:40
.= (P . (D \/ B)) - (P . B) by Th5 ;
then P . (E \ B) <= 0 by A6, A7, XREAL_1:47;
then A8: P . (E \ B) = 0 by PROB_1:def 8;
A c= E by A3, A5, XBOOLE_1:9;
hence ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) by A2, A8, XBOOLE_1:7; :: thesis: verum

end;

thus ( ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) implies A in COM (Sigma,P) ) :: thesis: verum

proof

given A1, A2 being set such that A9: A1 in Sigma and
A10: A2 in Sigma and
A11: A1 c= A and
A12: A c= A2 and
A13: P . (A2 \ A1) = 0 ; :: thesis: A in COM (Sigma,P)
reconsider A2 = A2 as Element of Sigma by A10;
reconsider A1 = A1 as Element of Sigma by A9;
set C = A \ A1;
A14: A \ A1 is thin of P

proof

reconsider D = A2 \ A1 as Element of Sigma ;
A15: A \ A1 c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A \ A1 or x in D )
assume x in A \ A1 ; :: thesis: x in D
then ( x in A & not x in A1 ) by XBOOLE_0:def 5;
hence x in D by A12, XBOOLE_0:def 5; :: thesis: verum

end;

then A \ A1 c= Omega by XBOOLE_1:1;
hence A \ A1 is thin of P by A13, A15, Def4; :: thesis: verum

end;

A = A1 \/ (A \ A1) by A11, XBOOLE_1:45;
hence A in COM (Sigma,P) by A14, Def5; :: thesis: verum

end;