theorem Th12: :: GROUP_1A:12
for G being addGroup
for f, g, h being Element of G holds
( h + f = g iff f = (- h) + g )