theorem Th17: :: GROUP_1A:352

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