let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st ( X overlaps Y or X overlaps Z ) holds
X overlaps Y (\/) Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( ( X overlaps Y or X overlaps Z ) implies X overlaps Y (\/) Z )
assume A1: ( X overlaps Y or X overlaps Z ) ; :: thesis: X overlaps Y (\/) Z

per cases ( X overlaps Y or X overlaps Z ) by A1;

suppose X overlaps Y ; :: thesis: X overlaps Y (\/) Z

then consider x being ManySortedSet of I such that
A2: x in X and
A3: x in Y by Th11;
x in Y (\/) Z by A3, Th7;
hence X overlaps Y (\/) Z by A2, Th10; :: thesis: verum

end;

suppose X overlaps Z ; :: thesis: X overlaps Y (\/) Z

then consider x being ManySortedSet of I such that
A4: x in X and
A5: x in Z by Th11;
x in Y (\/) Z by A5, Th7;
hence X overlaps Y (\/) Z by A4, Th10; :: thesis: verum

end;

end;