let a be Complex; :: thesis: -- {a} = {(- a)}
let z be Complex; :: according to MEMBERED:def 13 :: thesis: ( ( not z in -- {a} or z in {(- a)} ) & ( not z in {(- a)} or z in -- {a} ) )

hereby :: thesis: ( not z in {(- a)} or z in -- {a} )

assume z in -- {a} ; :: thesis: z in {(- a)}
then consider c being Complex such that
A1: z = - c and
A2: c in {a} ;
c = a by A2, TARSKI:def 1;
hence z in {(- a)} by A1, TARSKI:def 1; :: thesis: verum

end;

assume z in {(- a)} ; :: thesis: z in -- {a}
then A3: z = - a by TARSKI:def 1;
( a in COMPLEX & a in {a} ) by TARSKI:def 1, XCMPLX_0:def 2;
hence z in -- {a} by A3; :: thesis: verum