for G being Group holds rng (inverse_op G) = the carrier of G