let X be set ; :: thesis: ( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) )

now

assume that
A1: X <> {} and
A2: for a, b being set holds
( not a <> b or not a in X or not b in X ) ; :: thesis: ex a being set st {a} = X
consider p being Element of X;
for z being set holds
( z in X iff z = p ) by A1, A2;
then X = {p} by TARSKI:def 1;
hence ex a being set st {a} = X ; :: thesis: verum

end;

hence ( X = {} or ex a being set st
( {a} = X or ex a, b being set st
( a <> b & a in X & b in X ) ) ) ; :: thesis: verum