let F be Subset-Family of X; :: thesis: ( F is compl-closed & F is sigma-additive implies F is sigma-multiplicative )

assume that

A6: F is compl-closed and

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

let f be SetSequence of X; :: according to PROB_1:def 6 :: thesis: ( not rng f c= F or Intersection f in F )

assume A8: rng f c= F ; :: thesis: Intersection f in F

dom (Complement f) = NAT by FUNCT_2:def 1;

then reconsider M = rng (Complement f) as non empty V58() Subset-Family of X by CARD_3:93;

M c= F

hence Intersection f in F by A6; :: thesis: verum

assume that

A6: F is compl-closed and

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

let f be SetSequence of X; :: according to PROB_1:def 6 :: thesis: ( not rng f c= F or Intersection f in F )

assume A8: rng f c= F ; :: thesis: Intersection f in F

dom (Complement f) = NAT by FUNCT_2:def 1;

then reconsider M = rng (Complement f) as non empty V58() Subset-Family of X by CARD_3:93;

M c= F

proof

then
( Intersection f = (union M) ` & union M in F )
by A7, CARD_3:def 4;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in M or e in F )

assume e in M ; :: thesis: e in F

then consider n being object such that

A9: n in NAT and

A10: e = (Complement f) . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A9;

A11: f . n in rng f by NAT_1:51;

e = (f . n) ` by A10, PROB_1:def 2;

hence e in F by A6, A8, A11; :: thesis: verum

end;assume e in M ; :: thesis: e in F

then consider n being object such that

A9: n in NAT and

A10: e = (Complement f) . n by FUNCT_2:11;

reconsider n = n as Element of NAT by A9;

A11: f . n in rng f by NAT_1:51;

e = (f . n) ` by A10, PROB_1:def 2;

hence e in F by A6, A8, A11; :: thesis: verum

hence Intersection f in F by A6; :: thesis: verum