consider a being object such that
A1:
a in A
by XBOOLE_0:def 1;
reconsider A9 = A as non empty non trivial set ;
consider b being object such that
A2:
b in A9 \ {a}
by XBOOLE_0:def 1, ZFMISC_1:139;
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:32;
hence
not TWOELEMENTSETS A is empty
by A1, A2, A3, Th8; verum