theorem Th19: :: GROUP_1A:19
for G being addGroup
for g, h being Element of G holds
( g + h = h + g iff g + (- h) = (- h) + g )