theorem :: GROUP_1A:204
for G being addGroup holds (0). G is Abelian