for G being addGroup
for g, h being Element of G st h + g = 0_ G & g + h = 0_ G holds
g = - h by Def5;