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