theorem Th100: :: PBOOLE:100

for I being set
for X, Y, Z being ManySortedSet of I st X overlaps Y & X c= Z holds
Z overlaps Y