:: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def 6 :
for Omega being non empty set
for E being Subset-Family of Omega
for b₃ being Dynkin_System of Omega holds
( b₃ = generated_Dynkin_System E iff ( E c= b₃ & ( for D being Dynkin_System of Omega st E c= D holds
b₃ c= D ) ) );