let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds X (\) (Y (\/) Z) = (X (\) Y) (/\) (X (\) Z)
let X, Y, Z be ManySortedSet of I; :: thesis: X (\) (Y (\/) Z) = (X (\) Y) (/\) (X (\) Z)
thus X (\) (Y (\/) Z) = (X (\) Y) (\) Z by Th73
.= ((X (\) Y) (/\) X) (\) Z by Th56, Th23
.= (X (\) Y) (/\) (X (\) Z) by Th62 ; :: thesis: verum