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