let I be non empty set ; :: thesis: for X, Y being ManySortedSet of I st X overlapsoverlap Y holds
X meets Y
let X, Y be ManySortedSet of I; :: thesis: ( X overlapsoverlap Y implies X meets Y )
consider i being Element of I;
assume X overlapsoverlap Y ; :: thesis: X meets Y
then X . i meets Y . i by Def10;
hence X meets Y by Def11; :: thesis: verum