let X, Y be set ; ( card X c= card Y implies ex Z being set st
( Z c= Y & card Z = card X ) )
assume
card X c= card Y
; 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; ( Z c= Y & card Z = card X )
thus
( Z c= Y & card Z = card X )
by A, CARD_1:70; verum