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 Th17;
(X /\ Y) \ (X /\ Z) = ((X /\ Y) \ X) \/ ((X /\ Y) \ Z) by Th75
.= ([[0]] I) \/ ((X /\ Y) \ Z) by A1, Th58
.= (X /\ Y) \ Z by Th53 ;
hence X /\ (Y \ Z) = (X /\ Y) \ (X /\ Z) by Th68; :: thesis: verum