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