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 :: thesis: ( X <> {} & ( for a, b being set holds
( not a <> b or not a in X or not b in X ) ) implies ex a being set st {a} = X )

set p = the 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 object holds
( z in X iff z = the Element of X ) ;
then X = { the Element of X} 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