let Omega be non empty set ; :: thesis: for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
let E be Subset-Family of Omega; :: thesis: ( E is intersection_stable implies for D being Dynkin_System of Omega st E c= D holds
sigma E c= D )
assume A1: E is intersection_stable ; :: thesis: for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
reconsider G = generated_Dynkin_System E as Dynkin_System of Omega ;
G is intersection_stable by A1, Th22;
then A2: G is SigmaField of Omega by Th19;
let D be Dynkin_System of Omega; :: thesis: ( E c= D implies sigma E c= D )
assume E c= D ; :: thesis: sigma E c= D
then A3: G c= D by Def6;
E c= G by Def6;
then sigma E c= G by A2, PROB_1:def 9;
hence sigma E c= D by A3; :: thesis: verum