theorem :: RAMSEY_1:15

for n, k being Nat
for X being infinite set
for P being a_partition of the_subsets_of_card (n,X) st card P = k holds
ex H being Subset of X st
( H is infinite & H is_homogeneous_for P )