theorem Th12: :: GROUP_1A:347

for G being addGroup holds rng (add_inverse G) = the carrier of G