theorem Th13: :: GROUP_1A:348

for G being addGroup holds (add_inverse G) " = add_inverse G