:: deftheorem Def18 defines FinSequence-membered FINSEQ_1:def 18 :
for X being set holds
( X is FinSequence-membered iff for x being object st x in X holds
x is FinSequence );