for X, Y being set st X is finite & Y is finite & card Y = X holds
the_subsets_of_card (X,Y) = {Y} by Lm3;