theorem Th18: :: GROUP_1A:18

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