let I be set ; :: thesis: for Y, Z, X being ManySortedSet of I st not Y overlapsoverlap Z holds
not X /\ Y overlapsoverlap X /\ Z
let Y, Z, X be ManySortedSet of I; :: thesis: ( not Y overlapsoverlap Z implies not X /\ Y overlapsoverlap X /\ Z )
assume A1: not Y overlapsoverlap Z ; :: thesis: not X /\ Y overlapsoverlap X /\ Z
( X /\ Y c= Y & X /\ Z c= Z ) by Th17;
hence not X /\ Y overlapsoverlap X /\ Z by A1, Th110; :: thesis: verum