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 Th72
.= (X \ (Y \/ Z)) \/ ((Y \ X) \ Z) by Th73
.= (X \ (Y \/ Z)) \/ (Y \ (X \/ Z)) by Th73 ; :: thesis: verum