let Omega be non empty set ; :: thesis:
let D be non empty Subset-Family of Omega; :: thesis:
assume that
A1: D is Dynkin_System of Omega and
A2: D is intersection_stable ; :: thesis:
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:
assume A4: rng f c= D ; :: thesis:
A5: for n being Element of NAT holds (f . n) ` in D

proof

let n be Element of NAT ; :: thesis:
f . n in rng f by NAT_1:51;
hence (f . n) ` in D by A1, A4, Def5; :: thesis:

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 = (f . n) ` by PROB_1:def 2;
hence (Complement f) . n in D by A5; :: thesis:

end;

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

proof

let x be object ; :: thesis:
assume x in rng (Complement f) ; :: thesis:
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:

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:

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: