theorem Th9: :: TOPGRP_1:10

for G being Group
for A being Subset of G holds (inverse_op G) .: A = A "