let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds (X (/\) Y) (\) Z = (X (\) Z) (/\) (Y (\) Z)
let X, Y, Z be ManySortedSet of I; :: thesis: (X (/\) Y) (\) Z = (X (\) Z) (/\) (Y (\) Z)
A1: X (\) Z c= X by Th56;
thus (X (/\) Y) (\) Z = (X (\) Z) (/\) Y by Th62
.= (X (\) Z) (\) ((X (\) Z) (\) Y) by Th68
.= (X (\) Z) (\) (X (\) (Z (\/) Y)) by Th73
.= ((X (\) Z) (\) X) (\/) ((X (\) Z) (/\) (Z (\/) Y)) by Th64
.= (EmptyMS I) (\/) ((X (\) Z) (/\) (Z (\/) Y)) by A1, Th52
.= (X (\) Z) (/\) (Y (\/) Z) by Th22, Th43
.= (X (\) Z) (/\) ((Y (\) Z) (\/) Z) by Th67
.= ((X (\) Z) (/\) (Y (\) Z)) (\/) ((X (\) Z) (/\) Z) by Th32
.= ((X (\) Z) (/\) (Y (\) Z)) (\/) (EmptyMS I) by Th63
.= (X (\) Z) (/\) (Y (\) Z) by Th22, Th43 ; :: thesis: verum