theorem :: PZFMISC1:49

for I being set
for x, y, X being ManySortedSet of I st not I is empty & y in X (\) {x} holds
y <> x