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 Th62;
thus (X /\ Y) \ Z = (X \ Z) /\ Y by Th68
.= (X \ Z) \ ((X \ Z) \ Y) by Th74
.= (X \ Z) \ (X \ (Z \/ Y)) by Th79
.= ((X \ Z) \ X) \/ ((X \ Z) /\ (Z \/ Y)) by Th70
.= ([[0]] I) \/ ((X \ Z) /\ (Z \/ Y)) by A1, Th58
.= (X \ Z) /\ (Y \/ Z) by Th53
.= (X \ Z) /\ ((Y \ Z) \/ Z) by Th73
.= ((X \ Z) /\ (Y \ Z)) \/ ((X \ Z) /\ Z) by Th38
.= ((X \ Z) /\ (Y \ Z)) \/ ([[0]] I) by Th69
.= (X \ Z) /\ (Y \ Z) by Th53 ; :: thesis: verum