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