theorem Th20: :: GROUP_1A:221

for G being addGroup
for a being Element of G holds a * a = a