theorem Th9: :: CARD_1:10

for X, Y being set holds
( card X c= card Y iff ex f being Function st
( f is one-to-one & dom f = X & rng f c= Y ) )