theorem :: PBOOLE:123

for I being non empty set
for X, Y being ManySortedSet of I st X overlaps Y holds
X meets Y