theorem Th127: :: PBOOLE:127

for I being non empty set
for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds
not X overlaps Y