let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds X (/\) Y c= X (\/) Z
let X, Y, Z be ManySortedSet of I; :: thesis: X (/\) Y c= X (\/) Z
( X (/\) Y c= X & X c= X (\/) Z ) by Th14, Th15;
hence X (/\) Y c= X (\/) Z by Th13; :: thesis: verum