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