let X be set ; :: thesis: ( X is FinSequence-membered implies X is finite-membered )
assume A1: X is FinSequence-membered ; :: thesis: X is finite-membered
for x being set st x in X holds
x is finite by A1;
hence X is finite-membered by FINSET_1:def 6; :: thesis: verum