theorem :: GROUP_1A:203

for G being addGroup holds
( G is Abelian addGroup iff the addF of G is commutative )