let Omega be non empty set ; :: thesis:
let E be Subset-Family of Omega; :: thesis:
let X, Y be Subset of Omega; :: thesis:
assume A1: ( X in generated_Dynkin_System E & Y in generated_Dynkin_System E & 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
A2: for x being set holds
( x in h iff ( x in bool (bool Omega) & S₁[x] ) ) from XBOOLE_0:sch 1();
A3: for Y being set st Y in h holds
Y is Dynkin_System of Omega

let Y be set ; :: thesis:
assume Y in h ; :: thesis:
then ex X being Element of G st Y = DynSys X,G by A2;
hence Y is Dynkin_System of Omega ; :: thesis:

end;

not h is empty

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

end;

then reconsider h = h as non empty set ;
A4: meet h is Dynkin_System of Omega by A3, Th15;
for x being set st x in E holds
x in meet h

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

let Y be set ; :: thesis:
assume A6: Y in h ; :: thesis:
consider X being Element of G such that
A7: Y = DynSys X,G by A2, A6;
x /\ X in G by A1, A5, Th24;
hence x in Y by A5, A7, Def9; :: thesis:

end;

hence x in meet h by SETFAM_1:def 1; :: thesis:

end;

then E c= meet h by TARSKI:def 3;
then A8: G c= meet h by A4, Def8;
DynSys X,G in h by A1, A2;
then meet h c= DynSys X,G by SETFAM_1:4;
then G c= DynSys X,G by A8, XBOOLE_1:1;
hence X /\ Y in generated_Dynkin_System E by A1, Def9; :: thesis: