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 that
A1: X in E and
A2: Y in generated_Dynkin_System E and
A3: 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 Def6;
then reconsider X = X as Element of G by A1;
for x being object st x in E holds
x in DynSys (X,G)

proof

let x be object ; :: thesis: ( x in E implies x in DynSys (X,G) )
assume A4: x in E ; :: thesis: x in DynSys (X,G)
then reconsider x = x as Subset of Omega ;
A5: E c= G by Def6;
x /\ X in E by A1, A3, A4, FINSUB_1:def 2;
hence x in DynSys (X,G) by A5, Def7; :: thesis: verum

end;

then E c= DynSys (X,G) ;
then generated_Dynkin_System E c= DynSys (X,G) by Def6;
hence X /\ Y in generated_Dynkin_System E by A2, Def7; :: thesis: verum