all(X,exists(Y,(bp(Y) <=> X=Y) and berlin(X))).

~ all(X,all(Y,bp(X) and bp(Y) => X=Y)).