let G be addGroup; :: thesis: for g being Element of G holds - {g} = {(- g)}
let g be Element of G; :: thesis: - {g} = {(- g)}
thus - {g} c= {(- g)} :: according to XBOOLE_0:def 10 :: thesis: {(- g)} c= - {g}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in - {g} or x in {(- g)} )
assume x in - {g} ; :: thesis: x in {(- g)}
then consider h being Element of G such that
A1: x = - h and
A2: h in {g} ;
h = g by A2, TARSKI:def 1;
hence x in {(- g)} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(- g)} or x in - {g} )
assume x in {(- g)} ; :: thesis: x in - {g}
then A3: x = - g by TARSKI:def 1;
g in {g} by TARSKI:def 1;
hence x in - {g} by A3; :: thesis: verum