let I be set ; :: thesis: for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlapsoverlap Y
let x, X, Y be ManySortedSet of I; :: thesis: ( x in X & x in Y implies X overlapsoverlap Y )
assume A1: ( x in X & x in Y ) ; :: thesis: X overlapsoverlap Y
let i be set ; :: according to PBOOLE:def 10 :: thesis: ( i in I implies X . i meets Y . i )
assume i in I ; :: thesis: X . i meets Y . i
then ( x . i in X . i & x . i in Y . i ) by A1, Def4;
hence X . i meets Y . i by XBOOLE_0:3; :: thesis: verum