let n be Nat; :: thesis: for X being finite set st n <= card X holds
ex A being finite Subset of X st card A = n
let X be finite set ; :: thesis: ( n <= card X implies ex A being finite Subset of X st card A = n )
assume A1: n <= card X ; :: thesis: ex A being finite Subset of X st card A = n
consider p being FinSequence such that
A2: rng p = X and
A3: p is one-to-one by Th58;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
n <= len p by A1, A2, A3, Th62;
then A4: len q = n by FINSEQ_1:17;
reconsider A = rng q as Subset of X by A2, RELAT_1:70;
q is one-to-one by A3, FUNCT_1:52;
then card A = n by A4, Th62;
hence ex A being finite Subset of X st card A = n ; :: thesis: verum