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