let X be set ; :: thesis:
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:
assume that
Z in X and
Y c= X ; :: thesis:
given n being Nat such that A3: Y,n are_equipotent ; :: thesis:
A4: ( not Z in Y implies S₁[Y \/ {Z}] )

proof

assume A5: not Z in Y ; :: thesis:

now :: thesis:

set x = the Element of Y /\ {Z};
assume Y /\ {Z} <> {} ; :: thesis:
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:

end;

then A6: Y misses {Z} ;

A7: now :: thesis:

assume n meets {n} ; :: thesis:
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:

end;

take succ n ; :: thesis:
{Z},{n} are_equipotent by Th27;
hence Y \/ {Z}, succ n are_equipotent by A3, A7, A6, Th30; :: thesis:

end;

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

proof

assume A10: Z in Y ; :: thesis:
take n ; :: thesis:
thus Y \/ {Z},n are_equipotent by A3, A10, XBOOLE_1:12, ZFMISC_1:31; :: thesis:

end;

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

end;

assume A11: X is finite ; :: thesis:
thus S₁[X] from FINSET_1:sch 2(A11, A1, A2); :: thesis: