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

proof

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

end;

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