let X be set ; :: thesis: ( X is finite implies ex n being Nat st X,n are_equipotent )
defpred S₁[ set ] means ex n being Nat 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 Nat 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 :: thesis: not Y /\ {Z} <> {}

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

end;

then A6: Y misses {Z} ;

A7: now :: thesis: not n meets {n}

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

end;

take succ n ; :: thesis: Y \/ {Z}, succ n are_equipotent
{Z},{n} are_equipotent by Th27;
hence Y \/ {Z}, succ n are_equipotent by A3, A7, A6, Th30; :: 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
thus Y \/ {Z},n are_equipotent by A3, A10, XBOOLE_1:12, ZFMISC_1:31; :: thesis: verum

end;

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

end;

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