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 x' being Subset of such that
A2: x' = x and
A3: card x' = Z ;
reconsider x'' = x' as Subset of by A1, XBOOLE_1:1;
x'' = 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