let a be complex number ; :: thesis: -- {a} = {(- a)}
let z be complex number ; :: 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 Element of 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;
A4: a in COMPLEX by XCMPLX_0:def 2;
a in {a} by TARSKI:def 1;
hence z in -- {a} by A3, A4; :: thesis: verum