let a, b be complex number ; :: thesis: {a,b} "" = {(a " ),(b " )}
let z be complex number ; :: according to MEMBERED:def 13 :: thesis: ( ( not z in {a,b} "" or z in {(a " ),(b " )} ) & ( not z in {(a " ),(b " )} or z in {a,b} "" ) )

hereby :: thesis: ( not z in {(a " ),(b " )} or z in {a,b} "" )

assume z in {a,b} "" ; :: thesis: z in {(a " ),(b " )}
then consider c being Element of COMPLEX such that
A1: z = c " and
A2: c in {a,b} ;
( c = a or c = b ) by A2, TARSKI:def 2;
hence z in {(a " ),(b " )} by A1, TARSKI:def 2; :: thesis: verum

end;

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