let X be set ; :: thesis: for S being non empty Subset-Family of X holds
( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )
let S be non empty Subset-Family of X; :: thesis: ( ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) iff S is SigmaField of X )

hereby :: thesis: ( S is SigmaField of X implies ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) )

assume A1: ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) ; :: thesis: S is SigmaField of X
for M being N_Sub_set_fam of X st M c= S holds
union M in S

proof

let M be N_Sub_set_fam of X; :: thesis: ( M c= S implies union M in S )
assume A2: M c= S ; :: thesis: union M in S
A3: X \ M is N_Sub_set_fam of X by Th42;
X \ M c= S

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X \ M or y in S )
assume A4: y in X \ M ; :: thesis: y in S
then reconsider B = y as Subset of X ;
B ` in M by A4, SETFAM_1:def 8;
then (B ` ) ` in S by A1, A2;
hence y in S ; :: thesis: verum

end;

then X \ (meet (X \ M)) in S by A1, A3;
hence union M in S by Th15; :: thesis: verum

end;

then reconsider S' = S as non empty compl-closed sigma-additive Subset-Family of X by A1, Def3, Def9;
S' is SigmaField of X ;
hence S is SigmaField of X ; :: thesis: verum

end;

assume A5: S is SigmaField of X ; :: thesis: ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) )
for M being N_Sub_set_fam of X st M c= S holds
meet M in S

proof

let M be N_Sub_set_fam of X; :: thesis: ( M c= S implies meet M in S )
assume A6: M c= S ; :: thesis: meet M in S
A7: X \ M is N_Sub_set_fam of X by Th42;
X \ M c= S

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X \ M or y in S )
assume A8: y in X \ M ; :: thesis: y in S
then reconsider B = y as Subset of X ;
B ` in M by A8, SETFAM_1:def 8;
then (B ` ) ` in S by A5, A6, PROB_1:def 1;
hence y in S ; :: thesis: verum

end;

then union (X \ M) in S by A5, A7, Def9;
then X \ (union (X \ M)) in S by A5, Def3;
hence meet M in S by Th15; :: thesis: verum

end;

hence ( ( for A being set st A in S holds
X \ A in S ) & ( for M being N_Sub_set_fam of X st M c= S holds
meet M in S ) ) by A5, Def3; :: thesis: verum