theorem Th18: :: GROUP_1A:353

for G being addGroup
for a being Element of G holds (+ a) /" = + (- a)