let X, Y be set ; :: thesis: ( card X c= card Y implies ex Z being set st

( Z c= Y & card Z = card X ) )

assume card X c= card Y ; :: thesis: ex Z being set st

( Z c= Y & card Z = card X )

then consider f being Function such that

A: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take Z = rng f; :: thesis: ( Z c= Y & card Z = card X )

thus ( Z c= Y & card Z = card X ) by A, CARD_1:70; :: thesis: verum

( Z c= Y & card Z = card X ) )

assume card X c= card Y ; :: thesis: ex Z being set st

( Z c= Y & card Z = card X )

then consider f being Function such that

A: ( f is one-to-one & dom f = X & rng f c= Y ) by CARD_1:10;

take Z = rng f; :: thesis: ( Z c= Y & card Z = card X )

thus ( Z c= Y & card Z = card X ) by A, CARD_1:70; :: thesis: verum