let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X (\) (X (/\) Y) = X (\) Y
let X, Y be ManySortedSet of I; :: thesis: X (\) (X (/\) Y) = X (\) Y
thus X (\) (X (/\) Y) = (X (\) X) (\/) (X (\) Y) by Th69
.= (EmptyMS I) (\/) (X (\) Y) by Th52
.= X (\) Y by Th22, Th43 ; :: thesis: verum