theorem :: FINSEQ_4:72

for n being Nat
for X being finite set st n <= card X holds
ex A being finite Subset of X st card A = n