theorem Th13: :: TOPGRP_1:14

for G being Group holds (inverse_op G) " = inverse_op G