:: deftheorem defines are_isomorphic WAYBEL_1:def 8 :
for L1, L2 being RelStr holds
( L1,L2 are_isomorphic iff ex f being Function of L1,L2 st f is isomorphic );