theorem :: PZFMISC1:47

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