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: S₁[ 0 ]

proof

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

end;

A3: now

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

proof

assume A5: k + 1 <= card X ; :: thesis: ex Y being Subset of X st card Y = k + 1
then A6: k < card X by NAT_1:13;
consider Y being Subset of X such that
A7: card Y = k by A4, A5, NAT_1:13;
not X c= Y by A6, A7, XBOOLE_0:def 10;
then consider x being set such that
A8: ( x in X & not x in Y ) by TARSKI:def 3;
{x} c= X by A8, 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 A7, A8, CARD_2:54; :: thesis: verum

end;

end;

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