let X be set ; :: thesis: for S being non empty set holds
( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )
let S be non empty set ; :: thesis: ( S is SigmaField of X iff ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) )
thus ( S is SigmaField of X implies ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ) :: thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) implies S is SigmaField of X )

proof

assume S is SigmaField of X ; :: thesis: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) )
then reconsider S = S as SigmaField of X ;
for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S

proof

let A1 be SetSequence of X; :: thesis: ( rng A1 c= S implies Union A1 in S )
assume A1: rng A1 c= S ; :: thesis: Union A1 in S
reconsider A1 = A1 as SetSequence of by A1, RELAT_1:def 19;
Union A1 in S by PROB_1:46;
hence Union A1 in S ; :: thesis: verum

end;

hence ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) by PROB_1:32; :: thesis: verum

end;

assume A2: ( S c= bool X & ( for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S ) & ( for A being Subset of X st A in S holds
A ` in S ) ) ; :: thesis: S is SigmaField of X
for A1 being SetSequence of X st rng A1 c= S holds
Intersection A1 in S

proof

let A1 be SetSequence of X; :: thesis: ( rng A1 c= S implies Intersection A1 in S )
assume A3: rng A1 c= S ; :: thesis: Intersection A1 in S
for n being Nat holds (Complement A1) . n in S

proof

let n be Nat; :: thesis: (Complement A1) . n in S
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A1 . n in rng A1 by NAT_1:52;
then A1 . n in S by A3;
then (A1 . n1) ` in S by A2;
hence (Complement A1) . n in S by PROB_1:def 4; :: thesis: verum

end;

then rng (Complement A1) c= S by NAT_1:53;
then (Union (Complement A1)) ` in S by A2;
hence Intersection A1 in S by PROB_1:def 5; :: thesis: verum

end;

hence S is SigmaField of X by A2, PROB_1:32; :: thesis: verum