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