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)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_subsets_of_card (Z,X) or 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