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;

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

let y be object ; :: thesis: ( y in (add_inverse G) .: A implies y in - A )
assume y in (add_inverse 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 = (add_inverse G) . x by FUNCT_2:64;
reconsider x = x as Element of G by A1;
y = - x by A3, Def6;
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 (add_inverse G) .: A )
assume y in - A ; :: thesis: y in (add_inverse G) .: A
then consider g being Element of G such that
A4: ( y = - g & g in A ) ;
(add_inverse G) . g = - g by Def6;
hence y in (add_inverse G) .: A by A4, FUNCT_2:35; :: thesis: verum