theorem :: PZFMISC1:23

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