let Omega be non empty set ; :: thesis:
let E be Subset-Family of Omega; :: thesis:
let X, Y be Subset of Omega; :: thesis:
assume that
A1: X in generated_Dynkin_System E and
A2: Y in generated_Dynkin_System E and
A3: E is intersection_stable ; :: thesis:
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
defpred S₁[ set ] means ex X being Element of G st $1 = DynSys X,G;
consider h being set such that
A4: for x being set holds
( x in h iff ( x in bool (bool Omega) & S₁[x] ) ) from XBOOLE_0:sch 1();
A5: for Y being set st Y in h holds
Y is Dynkin_System of Omega

end;

consider X being Element of G;
DynSys X,G in h by A4;
hence not h is empty ; :: thesis:

end;

then reconsider h = h as non empty set ;
DynSys X,G in h by A1, A4;
then A6: meet h c= DynSys X,G by SETFAM_1:4;
for x being set st x in E holds
x in meet h

let x be set ; :: thesis:
assume A7: x in E ; :: thesis:
for Y being set st Y in h holds
x in Y

let Y be set ; :: thesis:
assume Y in h ; :: thesis:
then consider X being Element of G such that
A8: Y = DynSys X,G by A4;
x /\ X in G by A3, A7, Th24;
hence x in Y by A7, A8, Def9; :: thesis:

end;

end;