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

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

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

end;

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