for G being Group
for H being Subgroup of G holds inverse_op H = (inverse_op G) | the carrier of H