theorem TH9: :: GROUP_1A:9
for G being addGroup
for g, h being Element of G st - h = - g holds
h = g