let F be Subset-Family of X; :: thesis: ( F is compl-closed & F is sigma-multiplicative implies F is sigma-additive )
assume that
A1: F is compl-closed and
A2: F is sigma-multiplicative ; :: thesis: F is sigma-additive
let M be non empty countable Subset-Family of X; :: according to MEASURE1:def 5 :: thesis: ( M c= F implies union M in F )
assume A3: M c= F ; :: thesis: union M in F
consider f being SetSequence of X such that
A4: M = rng f by SUPINF_2:def 8;
for n being Nat holds (Complement f) . n in F

proof

let n be Nat; :: thesis: (Complement f) . n in F
reconsider n = n as Element of NAT by ORDINAL1:def 12;
( f . n in M & (Complement f) . n = (f . n) ` ) by A4, FUNCT_2:4, PROB_1:def 2;
hence (Complement f) . n in F by A1, A3; :: thesis: verum

end;

then rng (Complement f) c= F by NAT_1:52;
then A5: Intersection (Complement f) in F by A2;
(Intersection (Complement f)) ` = union M by A4, CARD_3:def 4;
hence union M in F by A1, A5; :: thesis: verum