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 c= X (\/) Y by Th14;
then A1: X c= X (/\) (X (\/) Y) by Th17;
X (/\) (X (\/) Y) c= X by Th15;
hence X (/\) (X (\/) Y) = X by A1, Lm1; :: thesis: verum