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

consider p being Element of X;
assume ( X <> {} & ( 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
then for z being set holds
( z in X iff z = p ) ;
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