let X be set ; :: thesis: ( X is finite implies ex n being natural number st X,n are_equipotent )
defpred S₁[ set ] means ex n being natural number st $1,n are_equipotent ;
A1: S₁[ {} ] ;
A2: for Z, Y being set st Z in X & Y c= X & S₁[Y] holds
S₁[Y \/ {Z}]

proof

let Z, Y be set ; :: thesis: ( Z in X & Y c= X & S₁[Y] implies S₁[Y \/ {Z}] )
assume that
Z in X and
Y c= X ; :: thesis: ( not S₁[Y] or S₁[Y \/ {Z}] )
given n being natural number such that A3: Y,n are_equipotent ; :: thesis: S₁[Y \/ {Z}]
A4: ( not Z in Y implies S₁[Y \/ {Z}] )

proof

assume A5: not Z in Y ; :: thesis: S₁[Y \/ {Z}]

now

consider x being Element of Y /\ {Z};
assume Y /\ {Z} <> {} ; :: thesis: contradiction
then ( x in Y & x in {Z} ) by XBOOLE_0:def 4;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

then A6: Y misses {Z} by XBOOLE_0:def 7;

A7: now

assume n meets {n} ; :: thesis: contradiction
then consider x being set such that
A8: x in n and
A9: x in {n} by XBOOLE_0:3;
x = n by A9, TARSKI:def 1;
hence contradiction by A8; :: thesis: verum

end;

take succ n ; :: thesis: Y \/ {Z}, succ n are_equipotent
{Z},{n} are_equipotent by Th48;
hence Y \/ {Z}, succ n are_equipotent by A3, A7, A6, Th58; :: thesis: verum

end;

( Z in Y implies S₁[Y \/ {Z}] )

proof

assume A10: Z in Y ; :: thesis: S₁[Y \/ {Z}]
take n ; :: thesis: Y \/ {Z},n are_equipotent
{Z} c= Y by A10, ZFMISC_1:37;
hence Y \/ {Z},n are_equipotent by A3, XBOOLE_1:12; :: thesis: verum

end;

hence S₁[Y \/ {Z}] by A4; :: thesis: verum

end;

assume A11: X is finite ; :: thesis: ex n being natural number st X,n are_equipotent
thus S₁[X] from FINSET_1:sch 2(A11, A1, A2); :: thesis: verum