for x being object
for D being set holds
( x in D ^omega iff x is XFinSequence of D ) by Def7;