theorem Th10: :: RAMSEY_1:10

for k being Nat
for X being finite set st k <= card X holds
ex Y being Subset of X st card Y = k