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