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