theorem :: PZFMISC1:51

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