theorem :: PBOOLE:105

for I being set
for X, Y, Z being ManySortedSet of I st not Y overlaps Z holds
not X (/\) Y overlaps X (/\) Z