:: deftheorem defines are_equipotent WELLORD2:def 4 :
for X, Y being set holds
( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) );