let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds COM M is complete
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds COM M is complete
let M be sigma_Measure of S; :: thesis: COM M is complete
for A being Subset of X
for B being set st B in COM (S,M) & A c= B & (COM M) . B = 0. holds
A in COM (S,M)

proof

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

proof

take {} ; :: thesis: ( {} in S & ex C1 being thin of M st A = {} \/ C1 )
consider B2 being set such that
A4: B2 in S and
A5: ex C2 being thin of M st B = B2 \/ C2 by A1, Def3;
A6: M . B2 = 0. by A3, A4, A5, Def5;
consider C2 being thin of M such that
A7: B = B2 \/ C2 by A5;
set C1 = (A /\ B2) \/ (A /\ C2);
consider D2 being set such that
A8: D2 in S and
A9: C2 c= D2 and
A10: M . D2 = 0. by Def2;
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 S & (A /\ B2) \/ (A /\ C2) c= O & M . O = 0. )

proof

reconsider B2 = B2, D2 = D2 as Element of S by A4, A8;
reconsider O1 = B2 \/ D2 as Element of S by A4, A8, FINSUB_1:def 1;
take B2 \/ D2 ; :: thesis: ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. )
( M . (B2 \/ D2) <= 0. + 0. & 0. <= M . O1 ) by A6, A10, MEASURE1:33, MEASURE1:def 2;
hence ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. ) by A11, XBOOLE_1:13, XXREAL_0:1; :: thesis: verum

end;

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

end;

hence A in COM (S,M) by Def3; :: thesis: verum

end;

hence COM M is complete ; :: thesis: verum