theorem Th11: :: GROUP_1A:346

for G being addGroup holds add_inverse G is one-to-one