let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is_complete COM Sigma,P
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds COM P is_complete COM Sigma,P
let P be Probability of Sigma; :: thesis: COM P is_complete COM Sigma,P
for A being Subset of Omega
for B being set st B in COM Sigma,P & A c= B & (COM P) . B = 0 holds
A in COM Sigma,P

proof

let A be Subset of Omega; :: thesis: for B being set st B in COM Sigma,P & A c= B & (COM P) . B = 0 holds
A in COM Sigma,P
let B be set ; :: thesis: ( B in COM Sigma,P & A c= B & (COM P) . B = 0 implies A in COM Sigma,P )
assume A1: B in COM Sigma,P ; :: thesis: ( not A c= B or not (COM P) . B = 0 or A in COM Sigma,P )
assume A2: ( A c= B & (COM P) . B = 0 ) ; :: thesis: A in COM Sigma,P
ex B1 being set st
( B1 in Sigma & ex C1 being thin of P st A = B1 \/ C1 )

proof

consider B2 being set such that
A3: ( B2 in Sigma & ex C2 being thin of P st B = B2 \/ C2 ) by A1, Def5;
consider C2 being thin of P such that
A4: B = B2 \/ C2 by A3;
A5: P . B2 = 0 by A2, A3, Def8;
consider D2 being set such that
A6: ( D2 in Sigma & C2 c= D2 & P . D2 = 0 ) by Def4;
set C1 = (A /\ B2) \/ (A /\ C2);
A7: A = A /\ (B2 \/ C2) by A2, A4, XBOOLE_1:28
.= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ;
set O = B2 \/ D2;
( A /\ B2 c= B2 & A /\ C2 c= C2 ) by XBOOLE_1:17;
then A8: ( A /\ B2 c= B2 & A /\ C2 c= D2 ) by A6, XBOOLE_1:1;
A9: (A /\ B2) \/ (A /\ C2) is thin of P

proof

ex O being set st
( O in Sigma & (A /\ B2) \/ (A /\ C2) c= O & P . O = 0 )

proof

reconsider O1 = B2 \/ D2 as Element of Sigma by A3, A6, PROB_1:41;
reconsider B2 = B2, D2 = D2 as Element of Sigma by A3, A6;
A11: P . (B2 \/ D2) <= 0 + 0 by A5, A6, PROB_1:75;
take B2 \/ D2 ; :: thesis: ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 )
thus ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 ) by A8, A11, PROB_1:def 13, XBOOLE_1:13; :: thesis: verum

end;

hence (A /\ B2) \/ (A /\ C2) is thin of P by Def4; :: thesis: verum

end;

take {} ; :: thesis: ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 )
thus ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 ) by A7, A9, PROB_1:42; :: thesis: verum

end;

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

end;

hence COM P is_complete COM Sigma,P by Def3; :: thesis: verum