let X be set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for D being non empty Subset-Family of X st ( for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
D is SigmaField of X

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for D being non empty Subset-Family of X st ( for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
D is SigmaField of X

let M be sigma_Measure of S; :: thesis: for D being non empty Subset-Family of X st ( for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) holds
D is SigmaField of X

let D be non empty Subset-Family of X; :: thesis: ( ( for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ) implies D is SigmaField of X )

assume A1: for A being set holds
( A in D iff ex B being set st
( B in S & ex C being thin of M st A = B \/ C ) ) ; :: thesis: D is SigmaField of X
A2: for K being N_Sub_set_fam of X st K c= D holds
union K in D
proof
let K be N_Sub_set_fam of X; :: thesis: ( K c= D implies union K in D )
consider F being sequence of (bool X) such that
A3: K = rng F by SUPINF_2:def 8;
assume A4: K c= D ; :: thesis: union K in D
A5: for n being Element of NAT holds F . n in D
proof
let n be Element of NAT ; :: thesis: F . n in D
F . n in K by ;
hence F . n in D by A4; :: thesis: verum
end;
A6: for n being Element of NAT ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C ) by A5, A1;
for n being Element of NAT holds F . n in COM (S,M)
proof
let n be Element of NAT ; :: thesis: F . n in COM (S,M)
ex B being set st
( B in S & ex C being thin of M st F . n = B \/ C ) by A6;
hence F . n in COM (S,M) by Def3; :: thesis: verum
end;
then A7: for n being object st n in NAT holds
F . n in COM (S,M) ;
A8: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as sequence of (COM (S,M)) by ;
consider G being sequence of S such that
A9: for n being Element of NAT holds G . n in MeasPart (F . n) by Th15;
consider H being sequence of (bool X) such that
A10: for n being Element of NAT holds H . n = (F . n) \ (G . n) by Th16;
A11: for n being Element of NAT holds
( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
proof
let n be Element of NAT ; :: thesis: ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M )
G . n in MeasPart (F . n) by A9;
hence ( G . n in S & G . n c= F . n & (F . n) \ (G . n) is thin of M ) by Def4; :: thesis: verum
end;
for n being Element of NAT holds H . n is thin of M
proof
let n be Element of NAT ; :: thesis: H . n is thin of M
(F . n) \ (G . n) is thin of M by A11;
hence H . n is thin of M by A10; :: thesis: verum
end;
then consider L being sequence of S such that
A12: for n being Element of NAT holds
( H . n c= L . n & M . (L . n) = 0. ) by Th17;
ex B being set st
( B in S & ex C being thin of M st union K = B \/ C )
proof
set B = union (rng G);
take union (rng G) ; :: thesis: ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C )
A13: union (rng G) c= union (rng F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng G) or x in union (rng F) )
assume x in union (rng G) ; :: thesis: x in union (rng F)
then consider Z being set such that
A14: x in Z and
A15: Z in rng G by TARSKI:def 4;
dom G = NAT by FUNCT_2:def 1;
then consider n being object such that
A16: n in NAT and
A17: Z = G . n by ;
reconsider n = n as Element of NAT by A16;
set P = F . n;
A18: G . n c= F . n by A11;
ex P being set st
( P in rng F & x in P )
proof
take F . n ; :: thesis: ( F . n in rng F & x in F . n )
thus ( F . n in rng F & x in F . n ) by ; :: thesis: verum
end;
hence x in union (rng F) by TARSKI:def 4; :: thesis: verum
end;
ex C being thin of M st union K = (union (rng G)) \/ C
proof
for A being set st A in rng L holds
A is measure_zero of M
proof
let A be set ; :: thesis: ( A in rng L implies A is measure_zero of M )
assume A19: A in rng L ; :: thesis: A is measure_zero of M
dom L = NAT by FUNCT_2:def 1;
then A20: ex n being object st
( n in NAT & A = L . n ) by ;
rng L c= S by MEASURE2:def 1;
then reconsider A = A as Element of S by A19;
M . A = 0. by ;
hence A is measure_zero of M by MEASURE1:def 7; :: thesis: verum
end;
then union (rng L) is measure_zero of M by MEASURE2:14;
then A21: M . (union (rng L)) = 0. by MEASURE1:def 7;
set C = () \ (union (rng G));
A22: union K = (() \ (union (rng G))) \/ ((union (rng F)) /\ (union (rng G))) by
.= (union (rng G)) \/ (() \ (union (rng G))) by ;
reconsider C = () \ (union (rng G)) as Subset of X ;
A23: C c= union (rng H)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in union (rng H) )
assume A24: x in C ; :: thesis: x in union (rng H)
then x in union (rng F) by ;
then consider Z being set such that
A25: x in Z and
A26: Z in rng F by TARSKI:def 4;
consider n being object such that
A27: n in NAT and
A28: Z = F . n by ;
reconsider n = n as Element of NAT by A27;
A29: not x in union (rng G) by ;
not x in G . n then A31: x in (F . n) \ (G . n) by ;
ex Z being set st
( x in Z & Z in rng H )
proof
take H . n ; :: thesis: ( x in H . n & H . n in rng H )
dom H = NAT by FUNCT_2:def 1;
hence ( x in H . n & H . n in rng H ) by ; :: thesis: verum
end;
hence x in union (rng H) by TARSKI:def 4; :: thesis: verum
end;
union (rng H) c= union (rng L)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng H) or x in union (rng L) )
assume x in union (rng H) ; :: thesis: x in union (rng L)
then consider Z being set such that
A32: x in Z and
A33: Z in rng H by TARSKI:def 4;
dom H = NAT by FUNCT_2:def 1;
then consider n being object such that
A34: n in NAT and
A35: Z = H . n by ;
reconsider n = n as Element of NAT by A34;
n in dom L by ;
then A36: L . n in rng L by FUNCT_1:def 3;
H . n c= L . n by A12;
hence x in union (rng L) by ; :: thesis: verum
end;
then C c= union (rng L) by A23;
then C is thin of M by ;
then consider C being thin of M such that
A37: union K = (union (rng G)) \/ C by A22;
take C ; :: thesis: union K = (union (rng G)) \/ C
thus union K = (union (rng G)) \/ C by A37; :: thesis: verum
end;
hence ( union (rng G) in S & ex C being thin of M st union K = (union (rng G)) \/ C ) ; :: thesis: verum
end;
hence union K in D by A1; :: thesis: verum
end;
for A being set st A in D holds
X \ A in D
proof
let A be set ; :: thesis: ( A in D implies X \ A in D )
assume A38: A in D ; :: thesis: X \ A in D
ex Q being set st
( Q in S & ex W being thin of M st X \ A = Q \/ W )
proof
consider B being set such that
A39: B in S and
A40: ex C being thin of M st A = B \/ C by ;
set P = X \ B;
consider C being thin of M such that
A41: A = B \/ C by A40;
consider G being set such that
A42: G in S and
A43: C c= G and
A44: M . G = 0. by Def2;
set Q = (X \ B) \ G;
A45: X \ A = (X \ B) \ C by ;
A46: ex W being thin of M st X \ A = ((X \ B) \ G) \/ W
proof
set W = (X \ B) /\ (G \ C);
(X \ B) /\ (G \ C) c= X \ B by XBOOLE_1:17;
then reconsider W = (X \ B) /\ (G \ C) as Subset of X by XBOOLE_1:1;
reconsider W = W as thin of M by ;
take W ; :: thesis: X \ A = ((X \ B) \ G) \/ W
thus X \ A = ((X \ B) \ G) \/ W by ; :: thesis: verum
end;
take (X \ B) \ G ; :: thesis: ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W )
X \ B in S by ;
hence ( (X \ B) \ G in S & ex W being thin of M st X \ A = ((X \ B) \ G) \/ W ) by ; :: thesis: verum
end;
hence X \ A in D by A1; :: thesis: verum
end;
then reconsider D9 = D as non empty compl-closed sigma-additive Subset-Family of X by ;
D9 is SigmaField of X ;
hence D is SigmaField of X ; :: thesis: verum