let Omega be non empty set ; :: thesis: for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let E be Subset-Family of Omega; :: thesis: for X, Y being Subset of Omega st X in E & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
let X, Y be Subset of Omega; :: thesis: ( X in E & Y in generated_Dynkin_System E & E is intersection_stable implies X /\ Y in generated_Dynkin_System E )
assume A1: ( X in E & Y in generated_Dynkin_System E & E is intersection_stable ) ; :: thesis: X /\ Y in generated_Dynkin_System E
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
E c= generated_Dynkin_System E by Def8;
then reconsider X = X as Element of G by A1;
for x being set st x in E holds
x in DynSys X,G

proof

let x be set ; :: thesis: ( x in E implies x in DynSys X,G )
assume A2: x in E ; :: thesis: x in DynSys X,G
then reconsider x = x as Subset of Omega ;
A3: x /\ X in E by A1, A2, FINSUB_1:def 2;
E c= G by Def8;
hence x in DynSys X,G by A3, Def9; :: thesis: verum

end;

then ( E c= DynSys X,G & DynSys X,G is Dynkin_System of Omega ) by TARSKI:def 3;
then generated_Dynkin_System E c= DynSys X,G by Def8;
hence X /\ Y in generated_Dynkin_System E by A1, Def9; :: thesis: verum