:: deftheorem Def38 defines isomorphic WAYBEL_0:def 38 :
for S, T being RelStr
for f being Function of S,T holds
( ( not S is empty & not T is empty implies ( f is isomorphic iff ( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) ) ) ) & ( ( S is empty or T is empty ) implies ( f is isomorphic iff ( S is empty & T is empty ) ) ) );