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 by Def10;
hence X meets Y by Def11; :: thesis: verum