let Omega be non empty set ; :: thesis: for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega
let D be non empty Subset-Family of Omega; :: thesis: ( D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega )
assume A1: ( D is Dynkin_System of Omega & D is intersection_stable ) ; :: thesis: D is SigmaField of Omega
then A2: for X being Subset of Omega st X in D holds
X ` in D by Def7;
for f being SetSequence of Omega st rng f c= D holds
Intersection f in D

proof

let f be SetSequence of Omega; :: thesis: ( rng f c= D implies Intersection f in D )
assume A3: rng f c= D ; :: thesis: Intersection f in D
A4: for n being Element of NAT holds (f . n) ` in D

proof

let n be Element of NAT ; :: thesis: (f . n) ` in D
f . n in rng f by NAT_1:52;
hence (f . n) ` in D by A1, Def7, A3; :: thesis: verum

end;

A5: for n being Element of NAT holds (Complement f) . n in D

proof

let n be Element of NAT ; :: thesis: (Complement f) . n in D
(Complement f) . n = (f . n) ` by PROB_1:def 4;
hence (Complement f) . n in D by A4; :: thesis: verum

end;

for x being set st x in rng (Complement f) holds
x in D

proof

let x be set ; :: thesis: ( x in rng (Complement f) implies x in D )
assume A6: x in rng (Complement f) ; :: thesis: x in D
consider z being set such that
A7: ( z in dom (Complement f) & x = (Complement f) . z ) by A6, FUNCT_1:def 5;
reconsider n = z as Element of NAT by A7, FUNCT_2:def 1;
x = (Complement f) . n by A7;
hence x in D by A5; :: thesis: verum

end;

then rng (Complement f) c= D by TARSKI:def 3;
then union (rng (Complement f)) in D by A1, Th20;
then Union (Complement f) in D ;
then (Union (Complement f)) ` in D by A1, Def7;
hence Intersection f in D by PROB_1:def 5; :: thesis: verum

end;

hence D is SigmaField of Omega by A2, PROB_1:32; :: thesis: verum