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