let X be set ; :: thesis:
let S be non empty Subset-Family of X; :: thesis:

hereby :: thesis:

assume that
A1: for A being set st A in S holds
X \ A in S and
A2: for M being N_Sub_set_fam of X st M c= S holds
meet M in S ; :: thesis:
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:
assume A3: M c= S ; :: thesis:
A4: X \ M c= S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: y in X \ M ; :: thesis:
then reconsider B = y as Subset of X ;
B ` in M by A5, SETFAM_1:def 7;
then (B `) ` in S by A1, A3;
hence y in S ; :: thesis:

end;

X \ M is N_Sub_set_fam of X by Th21;
then X \ (meet (X \ M)) in S by A1, A2, A4;
hence union M in S by Th4; :: thesis:

end;

then reconsider S9 = S as non empty compl-closed sigma-additive Subset-Family of X by A1, Def1, Def5;
S9 is SigmaField of X ;
hence S is SigmaField of X ; :: thesis:

end;

assume A6: S is SigmaField of X ; :: thesis:
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:
assume A7: M c= S ; :: thesis:
A8: X \ M c= S

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A9: y in X \ M ; :: thesis:
then reconsider B = y as Subset of X ;
B ` in M by A9, SETFAM_1:def 7;
then (B `) ` in S by A6, A7, PROB_1:def 1;
hence y in S ; :: thesis:

end;

X \ M is N_Sub_set_fam of X by Th21;
then union (X \ M) in S by A6, A8, Def5;
then X \ (union (X \ M)) in S by A6, Def1;
hence meet M in S by Th4; :: thesis:

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 A6, Def1; :: thesis: