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

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

suppose X overlapsoverlap Y ; :: thesis: X overlapsoverlap 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 overlapsoverlap Y \/ Z by A2, Th10; :: thesis: verum

end;

suppose X overlapsoverlap Z ; :: thesis: X overlapsoverlap 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 overlapsoverlap Y \/ Z by A4, Th10; :: thesis: verum

end;

end;