:: deftheorem Def5 defines Dynkin_System DYNKIN:def 5 :
for Omega being non empty set
for b₂ being Subset-Family of Omega holds
( b₂ is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b₂ & f is disjoint_valued holds
Union f in b₂ ) & ( for X being Subset of Omega st X in b₂ holds
X ` in b₂ ) & {} in b₂ ) );