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