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