let I be set ; :: thesis: for X, Y being ManySortedSet of I st X overlaps Y holds
ex x being ManySortedSet of I st
( x in X & x in Y )
let X, Y be ManySortedSet of I; :: thesis: ( X overlaps Y implies ex x being ManySortedSet of I st
( x in X & x in Y ) )
deffunc H₁( object ) -> set = (X . $1) /\ (Y . $1);
assume A1: X overlaps Y ; :: thesis: ex x being ManySortedSet of I st
( x in X & x in Y )
A2: for i being object st i in I holds
H₁(i) <> {} by XBOOLE_0:def 7, A1;
consider x being ManySortedSet of I such that
A3: for i being object st i in I holds
x . i in H₁(i) from PBOOLE:sch 1(A2);
take x ; :: thesis: ( x in X & x in Y )

now :: thesis: for i being object st i in I holds
x . i in X . i

let i be object ; :: thesis: ( i in I implies x . i in X . i )
assume i in I ; :: thesis: x . i in X . i
then x . i in (X . i) /\ (Y . i) by A3;
hence x . i in X . i by XBOOLE_0:def 4; :: thesis: verum

end;

hence x in X ; :: thesis: x in Y

now :: thesis: for i being object st i in I holds
x . i in Y . i

let i be object ; :: thesis: ( i in I implies x . i in Y . i )
assume i in I ; :: thesis: x . i in Y . i
then x . i in (X . i) /\ (Y . i) by A3;
hence x . i in Y . i by XBOOLE_0:def 4; :: thesis: verum

end;

hence x in Y ; :: thesis: verum