theorem :: GROUP_3:2

for G being Group holds
( G is commutative Group iff the multF of G is commutative )