theorem :: GROUP_1A:222

for G being addGroup
for a being Element of G holds
( a * (- a) = a & (- a) * a = - a ) by Th1;