now :: thesis: for x being object holds not x in TWOELEMENTSETS {a}
let x be object ; :: thesis: not x in TWOELEMENTSETS {a}
assume x in TWOELEMENTSETS {a} ; :: thesis: contradiction
then consider u, v being object such that
A1: u in {a} and
A2: v in {a} and
A3: u <> v and
x = {u,v} by Th8;
u = a by A1, TARSKI:def 1
.= v by A2, TARSKI:def 1 ;
hence contradiction by A3; :: thesis: verum
end;
hence TWOELEMENTSETS {a} is empty by XBOOLE_0:def 1; :: thesis: verum