:: deftheorem defines are_similar UNIALG_2:def 1 :
for U1, U2 being Universal_Algebra holds
( U1,U2 are_similar iff signature U1 = signature U2 );