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 that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; :: thesis: D is SigmaField of Omega
A3: 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 A4: rng f c= D ; :: thesis: Intersection f in D
A5: 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:51;
hence (f . n) ` in D by A1, A4, Def5; :: thesis: verum

end;

A6: 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 2;
hence (Complement f) . n in D by A5; :: thesis: verum

end;

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

proof

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

end;

then rng (Complement f) c= D ;
then Union (Complement f) in D by A1, A2, Th16;
then (Union (Complement f)) ` in D by A1, Def5;
hence Intersection f in D by PROB_1:def 3; :: thesis: verum

end;

for X being Subset of Omega st X in D holds
X ` in D by A1, Def5;
hence D is SigmaField of Omega by A3, PROB_1:15; :: thesis: verum