let G be Group; :: thesis: for A being Subset of G holds (inverse_op G) " A = A "
let A be Subset of G; :: thesis: (inverse_op G) " A = A "
set f = inverse_op G;
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def 1;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A " c= (inverse_op G) " A

let x be object ; :: thesis: ( x in (inverse_op G) " A implies x in A " )
assume A2: x in (inverse_op G) " A ; :: thesis: x in A "
then reconsider g = x as Element of G ;
(inverse_op G) . x in A by A2, FUNCT_1:def 7;
then ((inverse_op G) . g) " in A " ;
then (g ") " in A " by GROUP_1:def 6;
hence x in A " ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A " or x in (inverse_op G) " A )
assume x in A " ; :: thesis: x in (inverse_op G) " A
then consider g being Element of G such that
A3: ( x = g " & g in A ) ;
(inverse_op G) . (g ") = (g ") " by GROUP_1:def 6
.= g ;
hence x in (inverse_op G) " A by A1, A3, FUNCT_1:def 7; :: thesis: verum