:: deftheorem defines are_commutative LOPBAN_4:def 1 :
for X being non empty multMagma
for x, y being Element of X holds
( x,y are_commutative iff x * y = y * x );