let I be set ; :: thesis: for x, X, Y being ManySortedSet of I st x in X & x in Y holds
X overlaps Y
let x, X, Y be ManySortedSet of I; :: thesis: ( x in X & x in Y implies X overlaps Y )
assume A1: ( x in X & x in Y ) ; :: thesis: X overlaps Y
let i be object ; :: according to PBOOLE:def 7 :: 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;
hence X . i meets Y . i by XBOOLE_0:3; :: thesis: verum