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;

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

let y be object ; :: thesis: ( y in (inverse_op G) .: A implies y in A " )
assume y in (inverse_op G) .: A ; :: thesis: y in A "
then consider x being object such that
A1: x in the carrier of G and
A2: x in A and
A3: y = (inverse_op G) . x by FUNCT_2:64;
reconsider x = x as Element of G by A1;
y = x " by A3, GROUP_1:def 6;
hence y in A " by A2; :: thesis: verum

end;

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