let X, Y be set ; :: thesis: ( X c= Y implies card X c= card Y )
assume A1: X c= Y ; :: thesis: card X c= card Y
ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y )
proof
take id X ; :: thesis: ( id X is one-to-one & dom (id X) = X & rng (id X) c= Y )
thus ( id X is one-to-one & dom (id X) = X & rng (id X) c= Y ) by A1, RELAT_1:45; :: thesis: verum
end;
hence card X c= card Y by Th9; :: thesis: verum