let A be non trivial set ; not TWOELEMENTSETS A is empty
consider a being set such that
A1:
a in A
by XBOOLE_0:def 1;
reconsider A9 = A as non empty non trivial set ;
A9 \ {a} is non empty set
by REALSET1:4;
then consider b being set such that
A2:
b in A9 \ {a}
by XBOOLE_0:def 1;
not b in {a}
by A2, XBOOLE_0:def 5;
then A3:
a <> b
by TARSKI:def 1;
{a,b} c= A
by A1, A2, ZFMISC_1:38;
hence
not TWOELEMENTSETS A is empty
by A1, A2, A3, Th10; verum