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 8 :: thesis: ( not proj2 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 V44() Subset-Family of X by CARD_3:127, RELAT_1:65;
M c= F

proof

let e be set ; :: 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 set such that
A9: n in NAT and
A10: e = (Complement f) . n by FUNCT_2:17;
reconsider n = n as Element of NAT by A9;
A11: f . n in rng f by NAT_1:52;
e = (f . n) ` by A10, PROB_1:def 4;
hence e in F by A6, A8, A11, PROB_1:def 1; :: thesis: verum

end;

then ( Intersection f = (union M) ` & union M in F ) by A7, Def9, CARD_3:def 4;
hence Intersection f in F by A6, PROB_1:def 1; :: thesis: verum