theorem ThB30: :: GROUP_1A:231

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