:: deftheorem defines are_epsilon-isomorphic ZF_COLLA:def 3 :
for X, Y being set holds
( X,Y are_epsilon-isomorphic iff ex f being Function st f is_epsilon-isomorphism_of X,Y );