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)

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

hence
COM M is complete
; :: thesis: verum
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 )

end;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

hence
A in COM (S,M)
by Def3; :: thesis: verum
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. )

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;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

then A12:
(A /\ B2) \/ (A /\ C2) is thin of M
by Def2;
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;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

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