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

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