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)
thus (X /\ Y) /\ Z = X /\ (Y /\ (Z /\ Z)) by Th29
.= X /\ ((Z /\ Y) /\ Z) by Th29
.= (X /\ Z) /\ (Y /\ Z) by Th29 ; :: thesis: verum