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 )

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

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: verum

( ( ( 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 A6:
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 ) ) )

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: S is SigmaField of X

for M being N_Sub_set_fam of X st M c= S holds

union M in S

S9 is SigmaField of X ;

hence S is SigmaField of X ; :: thesis: verum

end;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: S is SigmaField of X

for M being N_Sub_set_fam of X st M c= S holds

union M in S

proof

then reconsider S9 = S as non empty compl-closed sigma-additive Subset-Family of X by A1, Def1, Def5;
let M be N_Sub_set_fam of X; :: thesis: ( M c= S implies union M in S )

assume A3: M c= S ; :: thesis: union M in S

A4: X \ M c= S

then X \ (meet (X \ M)) in S by A1, A2, A4;

hence union M in S by Th4; :: thesis: verum

end;assume A3: M c= S ; :: thesis: union M in S

A4: X \ M c= S

proof

X \ M is N_Sub_set_fam of X
by Th21;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X \ M or y in S )

assume A5: y in X \ M ; :: thesis: y in S

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: verum

end;assume A5: y in X \ M ; :: thesis: y in S

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: verum

then X \ (meet (X \ M)) in S by A1, A2, A4;

hence union M in S by Th4; :: thesis: verum

S9 is SigmaField of X ;

hence S is SigmaField of X ; :: thesis: verum

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

hence
( ( for A being set st A in S holds
let M be N_Sub_set_fam of X; :: thesis: ( M c= S implies meet M in S )

assume A7: M c= S ; :: thesis: meet M in S

A8: X \ M c= S

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: verum

end;assume A7: M c= S ; :: thesis: meet M in S

A8: X \ M c= S

proof

X \ M is N_Sub_set_fam of X
by Th21;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X \ M or y in S )

assume A9: y in X \ M ; :: thesis: y in S

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: verum

end;assume A9: y in X \ M ; :: thesis: y in S

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: verum

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: verum

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: verum