theorem :: PZFMISC1:19

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