let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I st X overlapsoverlap Y & Y c= Z holds
X overlapsoverlap Z
let X, Y, Z be ManySortedSet of I; :: thesis: ( X overlapsoverlap Y & Y c= Z implies X overlapsoverlap Z )
assume that
A1: X overlapsoverlap Y and
A2: Y c= Z ; :: thesis: X overlapsoverlap Z
consider x being ManySortedSet of I such that
A3: x in X and
A4: x in Y by A1, Th11;
x in Z by A2, A4, Th9;
hence X overlapsoverlap Z by A3, Th10; :: thesis: verum