:: deftheorem Def12 defines associative MONOID_0:def 12 :
for G being non empty multMagma holds
( G is associative iff the multF of G is associative );