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)
A1: X (/\) Y c= X by Th15;
(X (/\) Y) (\) (X (/\) Z) = ((X (/\) Y) (\) X) (\/) ((X (/\) Y) (\) Z) by Th69
.= (EmptyMS I) (\/) ((X (/\) Y) (\) Z) by A1, Th52
.= (X (/\) Y) (\) Z by Th22, Th43 ;
hence X (/\) (Y (\) Z) = (X (/\) Y) (\) (X (/\) Z) by Th62; :: thesis: verum