theorem Th17: :: GROUP_1A:17

for G being addGroup
for g, h being Element of G holds
( g + h = h + g iff - (g + h) = (- g) + (- h) )