theorem Th3: :: ALGSTR_2:3

for G being non empty left_add-cancelable add-right-invertible Abelian addLoopStr
for a being Element of G holds - (- a) = a