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