theorem :: RAMSEY_1:5

for X being set holds the_subsets_of_card (0,X) = {0} by Lm2;