let I be set ; :: thesis: for X, Y, Z being ManySortedSet of I holds X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
let X, Y, Z be ManySortedSet of I; :: thesis: X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z)
A1: X /\ Y c= X by Th15;
(X /\ Y) \ (X /\ Z) = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Th69
.= ([[0]] I) \/ ((X /\ Y) \ Z) by A1, Th52
.= (X /\ Y) \ Z by Th22, Th43 ;
hence X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th62; :: thesis: verum