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