let X be finite set ; :: thesis: for n being Nat st n <= card X holds
ex Y being Subset of X st card Y = n
let n be Nat; :: thesis: ( n <= card X implies ex Y being Subset of X st card Y = n )
assume A1: n <= card X ; :: thesis: ex Y being Subset of X st card Y = n
defpred S₁[ Nat] means ( $1 <= card X implies ex Y being Subset of X st card Y = $1 );

A2: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

assume A4: k + 1 <= card X ; :: thesis: ex Y being Subset of X st card Y = k + 1
then consider Y being Subset of X such that
A5: card Y = k by A3, NAT_1:13;
k < card X by A4, NAT_1:13;
then not X c= Y by A5, XBOOLE_0:def 10;
then consider x being set such that
A6: x in X and
A7: not x in Y by TARSKI:def 3;
{x} c= X by A6, ZFMISC_1:37;
then reconsider Z = Y \/ {x} as Subset of X by XBOOLE_1:8;
take Z ; :: thesis: card Z = k + 1
thus card Z = k + 1 by A5, A7, CARD_2:54; :: thesis: verum

end;

end;

A8: S₁[ 0 ]

proof

reconsider e = {} as Subset of X by XBOOLE_1:2;
assume 0 <= card X ; :: thesis: ex Y being Subset of X st card Y = 0
take e ; :: thesis: card e = 0
thus card e = 0 ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A2);
hence ex Y being Subset of X st card Y = n by A1; :: thesis: verum