let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X (\/) (X (/\) Y) = X
let X, Y be ManySortedSet of I; :: thesis: X (\/) (X (/\) Y) = X
X (/\) Y c= X by Th15;
then A1: X (\/) (X (/\) Y) c= X by Th16;
X c= X (\/) (X (/\) Y) by Th14;
hence X (\/) (X (/\) Y) = X by A1, Lm1; :: thesis: verum