:: deftheorem Def3 defines associative GROUP_1:def 3 :
for IT being multMagma holds
( IT is associative iff for x, y, z being Element of IT holds (x * y) * z = x * (y * z) );