theorem Th22: :: GROUP_1:23

for G being Group holds inverse_op G is_an_inverseOp_wrt the multF of G