reconsider S = {{},X} as non empty Subset-Family of X by PROB_1:8;

take S ; :: thesis: ( not S is empty & S is compl-closed & S is sigma-additive )

thus not S is empty ; :: thesis: ( S is compl-closed & S is sigma-additive )

thus for A being set st A in S holds

X \ A in S :: according to MEASURE1:def 1 :: thesis: S is sigma-additive

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

A4: ( not X in M implies union M in S )

take S ; :: thesis: ( not S is empty & S is compl-closed & S is sigma-additive )

thus not S is empty ; :: thesis: ( S is compl-closed & S is sigma-additive )

thus for A being set st A in S holds

X \ A in S :: according to MEASURE1:def 1 :: thesis: S is sigma-additive

proof

let M be N_Sub_set_fam of X; :: according to MEASURE1:def 5 :: thesis: ( M c= S implies union M in S )
let A be set ; :: thesis: ( A in S implies X \ A in S )

A1: ( A = {} implies X \ A in S ) by TARSKI:def 2;

A2: ( A = X implies X \ A in S )

hence X \ A in S by A1, A2, TARSKI:def 2; :: thesis: verum

end;A1: ( A = {} implies X \ A in S ) by TARSKI:def 2;

A2: ( A = X implies X \ A in S )

proof

assume
A in S
; :: thesis: X \ A in S
assume
A = X
; :: thesis: X \ A in S

then X \ A = {} by XBOOLE_1:37;

hence X \ A in S by TARSKI:def 2; :: thesis: verum

end;then X \ A = {} by XBOOLE_1:37;

hence X \ A in S by TARSKI:def 2; :: thesis: verum

hence X \ A in S by A1, A2, TARSKI:def 2; :: thesis: verum

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

A4: ( not X in M implies union M in S )

proof

( X in M implies union M in S )
assume
not X in M
; :: thesis: union M in S

then for A being set st A in M holds

A c= {} by A3, TARSKI:def 2;

then union M c= {} by ZFMISC_1:76;

then union M = {} ;

hence union M in S by TARSKI:def 2; :: thesis: verum

end;then for A being set st A in M holds

A c= {} by A3, TARSKI:def 2;

then union M c= {} by ZFMISC_1:76;

then union M = {} ;

hence union M in S by TARSKI:def 2; :: thesis: verum

proof

hence
union M in S
by A4; :: thesis: verum
assume
X in M
; :: thesis: union M in S

then X c= union M by ZFMISC_1:74;

then X = union M ;

hence union M in S by TARSKI:def 2; :: thesis: verum

end;then X c= union M by ZFMISC_1:74;

then X = union M ;

hence union M in S by TARSKI:def 2; :: thesis: verum