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
.= ([[0]] 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)) \/ ([[0]] I) by Th63
.= (X \ Z) /\ (Y \ Z) by Th22, Th43 ; :: thesis: verum