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