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