let I be set ; :: thesis: for X, Z, V being ManySortedSet of I st X overlaps Z & X c= V holds
X overlaps Z (/\) V
let X, Z, V be ManySortedSet of I; :: thesis: ( X overlaps Z & X c= V implies X overlaps Z (/\) V )
assume that
A1: X overlaps Z and
A2: X c= V ; :: thesis: X overlaps 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 overlaps Z (/\) V by A3, Th10; :: thesis: verum