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