let Y be Subset of X; :: thesis: Y is FinSequence-membered
let x be set ; :: according to FINSEQ_1:def 19 :: thesis: ( x in Y implies x is FinSequence )
assume x in Y ; :: thesis: x is FinSequence
then x in X ;
hence x is FinSequence ; :: thesis: verum