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