:: deftheorem Def1 defines seqIntersection DYNKIN:def 1 :
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega
for b₄ being SetSequence of Omega holds
( b₄ = seqIntersection (X,f) iff for n being Element of NAT holds b₄ . n = X /\ (f . n) );