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 Th73;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:19;
n <= len p by A1, A2, A3, Th77;
then A4: len q = n by FINSEQ_1:21;
reconsider A = rng q as Subset of X by A2, RELAT_1:99;
q is one-to-one by A3, FUNCT_1:84;
then card A = n by A4, Th77;
hence ex A being finite Subset of X st card A = n ; :: thesis: verum