:: deftheorem Def12 defines commutative GROUP_1:def 12 :
for IT being multMagma holds
( IT is commutative iff for x, y being Element of IT holds x * y = y * x );