theorem Th12: :: TOPGRP_1:13

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