theorem Th11: :: TOPGRP_1:12

for G being Group holds inverse_op G is one-to-one