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