let a, b be Complex; :: thesis: {a,b} "" = {(a "),(b ")}
let z be Complex; :: 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 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;
thus z in {a,b} "" by A4, A3; :: thesis: verum