theorem :: GROUP_1A:204

for G being addGroup holds (0). G is Abelian