:: deftheorem Def11 defines commutative MONOID_0:def 11 :
for G being non empty multMagma holds
( G is commutative iff the multF of G is commutative );