theorem :: PZFMISC1:48

for I being set
for x, y, X being ManySortedSet of I st y in X (\) {x} holds
y in X