theorem Th31: :: GROUP_1A:31

for G being addGroup
for h being Element of G holds (- 1) * h = - h