let X, Y, Z be set ; :: thesis: ( X c= Y implies the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) )
assume A1: X c= Y ; :: thesis: the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y)
for x being set st x in the_subsets_of_card (Z,X) holds
x in the_subsets_of_card (Z,Y)

proof

let x be set ; :: thesis: ( x in the_subsets_of_card (Z,X) implies x in the_subsets_of_card (Z,Y) )
assume x in the_subsets_of_card (Z,X) ; :: thesis: x in the_subsets_of_card (Z,Y)
then consider x9 being Subset of X such that
A2: x9 = x and
A3: card x9 = Z ;
reconsider x99 = x9 as Subset of Y by A1, XBOOLE_1:1;
x99 = x by A2;
hence x in the_subsets_of_card (Z,Y) by A3; :: thesis: verum

end;

hence the_subsets_of_card (Z,X) c= the_subsets_of_card (Z,Y) by TARSKI:def 3; :: thesis: verum