let a be set ; :: thesis: TWOELEMENTSETS {a} = {}

now

let x be set ; :: thesis: not x in TWOELEMENTSETS {a}
assume x in TWOELEMENTSETS {a} ; :: thesis: contradiction
then consider u, v being set such that
A1: ( u in {a} & v in {a} & u <> v & x = {u,v} ) by Th10;
u = a by A1, TARSKI:def 1
.= v by A1, TARSKI:def 1 ;
hence contradiction by A1; :: thesis: verum

end;

hence TWOELEMENTSETS {a} = {} by XBOOLE_0:def 1; :: thesis: verum