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
proof
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;
then ( Intersection f = (union M) ` & union M in F ) by A7, CARD_3:def 4;
hence Intersection f in F by A6; :: thesis: verum