let E be Element of Fin X; :: thesis: E is FinSequence-membered
E c= X by FINSUB_1:def 5;
hence E is FinSequence-membered ; :: thesis: verum