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 rng A1 c= S ; :: thesis: Union A1 in S
then reconsider A1 = A1 as SetSequence of S by RELAT_1:def 19;
Union A1 in S by PROB_1:17;
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:15; :: thesis: verum

end;

assume that
A1: S c= bool X and
A2: for A1 being SetSequence of X st rng A1 c= S holds
Union A1 in S and
A3: 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 A4: 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 12;
A1 . n in rng A1 by NAT_1:51;
then (A1 . n1) ` in S by A3, A4;
hence (Complement A1) . n in S by PROB_1:def 2; :: thesis: verum

end;

then rng (Complement A1) c= S by NAT_1:52;
then (Union (Complement A1)) ` in S by A2, A3;
hence Intersection A1 in S by PROB_1:def 3; :: thesis: verum

end;

hence S is SigmaField of X by A1, A3, PROB_1:15; :: thesis: verum