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 ;
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 ;
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 ;
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 ;
hence ( B2 \/ D2 in S & (A /\ B2) \/ (A /\ C2) c= B2 \/ D2 & M . (B2 \/ D2) = 0. ) by ; :: thesis: verum
end;
then A12: (A /\ B2) \/ (A /\ C2) is thin of M by Def2;
A = A /\ (B2 \/ C2) by
.= {} \/ ((A /\ B2) \/ (A /\ C2)) by XBOOLE_1:23 ;
hence ( {} in S & ex C1 being thin of M st A = {} \/ C1 ) by ; :: thesis: verum
end;
hence A in COM (S,M) by Def3; :: thesis: verum
end;
hence COM M is complete ; :: thesis: verum