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