theorem :: RAMSEY_1:7

for X, Y, Z being set st X c= Y holds
the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by Lm1;