let Omega be non empty set ; :: thesis: for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
let E be Subset-Family of Omega; :: thesis: ( E is intersection_stable implies generated_Dynkin_System E is intersection_stable )
assume A1: E is intersection_stable ; :: thesis: generated_Dynkin_System E is intersection_stable
reconsider G = generated_Dynkin_System E as Subset-Family of Omega ;
for a, b being set st a in G & b in G holds
a /\ b in G by A1, Th21;
hence generated_Dynkin_System E is intersection_stable by FINSUB_1:def 2; :: thesis: verum