for X, Y being set holds
( card X c= card Y iff ex f being Function st X c= f .: Y )