exists(X,exists(Y,~(X=Y) and all(Z,(Z=X or Z=Y)))).
~(exists(Z,all(X,exists(W,all(Y,p(X,Y) == (Y=W))) == (X=Z))) ==
exists(W,all(Y,exists(Z,all(X,p(X,Y)== (X=Z))) == (Y=W)))).