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
proof
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 )
proof
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;
assume A in S ; :: thesis: X \ A in S
hence X \ A in S by A1, A2, TARSKI:def 2; :: thesis: verum
end;
let M be N_Sub_set_fam of X; :: according to MEASURE1:def 5 :: thesis: ( M c= S implies union M in S )
assume A3: M c= S ; :: thesis: union M in S
A4: ( not X in M implies union M in S )
proof
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;
( X in M implies union M in S )
proof
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;
hence union M in S by A4; :: thesis: verum