:: deftheorem defines are_isomorphic ALG_1:def 5 :
for U1, U2 being Universal_Algebra holds
( U1,U2 are_isomorphic iff ex f being Function of U1,U2 st f is_isomorphism );