theorem :: PZFMISC1:22

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