theorem Th29: :: GROUP_1A:230

for G being addGroup
for a, b being Element of G st G is Abelian addGroup holds
a * b = a