:: deftheorem Def3 defines OMEGA CATALAN2:def 3 :
for D being set
for b₂ being functional non empty set holds
( b₂ is OMEGA of D iff for x being set st x in b₂ holds
x is XFinSequence of D );