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 V58() 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

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

assume that

A1: F is compl-closed and

A2: F is sigma-multiplicative ; :: thesis: F is sigma-additive

let M be non empty V58() 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

then
rng (Complement f) c= F
by NAT_1:52;
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;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

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