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 & ex C being thin of P st A = B \/ C ) by Def5;
consider C being thin of P such that
A2: A = B \/ C by A1;
consider D being set such that
A3: ( D in Sigma & C c= D & P . D = 0 ) by Def4;
reconsider D = D as Event of Sigma by A3;
reconsider B = B as Event of Sigma by A1;
reconsider E = D \/ B as Event of Sigma ;
A5: A c= E by A2, A3, XBOOLE_1:9;
A6: P . (E \ B) = P . (D \ B) by XBOOLE_1:40
.= (P . (D \/ B)) - (P . B) by Th6 ;
P . (D \/ B) <= (P . D) + (P . B) by PROB_1:75;
then P . (E \ B) <= 0 by A3, A6, XREAL_1:49;
then P . (E \ B) = 0 by PROB_1:def 13;
hence ex A1, A2 being set st
( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) by A1, A5, 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 A7: ( A1 in Sigma & A2 in Sigma & A1 c= A & A c= A2 & P . (A2 \ A1) = 0 ) ; :: thesis: A in COM Sigma,P
reconsider A1 = A1 as Element of Sigma by A7;
reconsider A2 = A2 as Element of Sigma by A7;
set C = A \ A1;
A8: A = A1 \/ (A \ A1) by A7, XBOOLE_1:45;
A \ A1 is thin of P

proof

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

proof

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

end;

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

end;

hence A in COM Sigma,P by A8, Def5; :: thesis: verum

end;