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 XFAMILY:sch 1();
A5: for Y being set st Y in h holds
Y is Dynkin_System of Omega

end;

set X = the Element of G;
DynSys ( the Element of G,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:3;
for x being object st x in E holds
x in meet h

let x be object ; :: thesis:
reconsider xx = x as set by TARSKI:1;
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;
xx /\ X in G by A3, A7, Th20;
hence x in Y by A7, A8, Def7; :: thesis:

end;

end;