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 )
set i = the Element of I;
assume X overlaps Y ; :: thesis: X meets Y
then X . the Element of I meets Y . the Element of I ;
hence X meets Y ; :: thesis: verum