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) by Th100
.= X \+\ (Y \+\ (X /\ Y)) by Th102
.= (X \+\ Y) \+\ (X /\ Y) by Th98 ; :: thesis: verum