let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X overlapsoverlap Y /\ Z holds
( X overlapsoverlap Y & X overlapsoverlap Z )
let X, Y, Z be ManySortedSet of I; :: thesis: ( X overlapsoverlap Y /\ Z implies ( X overlapsoverlap Y & X overlapsoverlap Z ) )
assume X overlapsoverlap Y /\ Z ; :: thesis: ( X overlapsoverlap Y & X overlapsoverlap Z )
then consider x being ManySortedSet of I such that
A1: x in X and
A2: x in Y /\ Z by Th11;
( x in Y & x in Z ) by A2, Th8;
hence ( X overlapsoverlap Y & X overlapsoverlap Z ) by A1, Th10; :: thesis: verum