theorem Th22: :: GROUP_1A:22

for G being addGroup holds add_inverse G is_an_inverseOp_wrt the addF of G