let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma holds COM P is complete
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma holds COM P is complete
let P be Probability of Sigma; :: thesis: COM P is complete
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 that
A2: A c= B and
A3: (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

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

proof

reconsider B2 = B2, D2 = D2 as Element of Sigma by A4, A8;
take B2 \/ D2 ; :: thesis: ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 )
P . (B2 \/ D2) <= 0 + 0 by A6, A10, PROB_1:39;
hence ( B2 \/ D2 in Sigma & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & P . (B2 \/ D2) = 0 ) by A11, PROB_1:def 8, XBOOLE_1:13; :: thesis: verum

end;

then A12: (A /\ B2) \/ (A /\ C2) is thin of P by Def4;
A = A /\ (B2 \/ C2) by A2, A7, XBOOLE_1:28
.= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ;
hence ( {} in Sigma & ex C1 being thin of P st A = {} \/ C1 ) by A12, PROB_1:4; :: thesis: verum

end;

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

end;

hence COM P is complete ; :: thesis: verum