theorem Th10: :: PBOOLE:10

for I being set
for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlaps Y