:: deftheorem Def7 defines DynSys DYNKIN:def 7 :
for Omega being non empty set
for G being set
for X being Subset of Omega
for b₄ being Subset-Family of Omega holds
( b₄ = DynSys (X,G) iff for A being Subset of Omega holds
( A in b₄ iff A /\ X in G ) );