theorem :: GROUP_1A:23

for G being addGroup holds the_inverseOp_wrt the addF of G = add_inverse G