theorem Th16: :: GROUP_1A:16
for G being addGroup
for g, h being Element of G holds - (h + g) = (- g) + (- h)