theorem Th3: :: COMBGRAS:3

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