let I be set ; :: thesis: for X, Y, Z, V being ManySortedSet of I st X c= Y & Z c= V & X overlaps Z holds
Y overlaps V
let X, Y, Z, V be ManySortedSet of I; :: thesis: ( X c= Y & Z c= V & X overlaps Z implies Y overlaps V )
assume that
A1: X c= Y and
A2: Z c= V ; :: thesis: ( not X overlaps Z or Y overlaps V )
assume X overlaps Z ; :: thesis: Y overlaps V
then Y overlaps Z by A1, Th100;
hence Y overlaps V by A2, Th99; :: thesis: verum