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 Th28
.= ((X \ Y) \/ Y) \/ X by Th67
.= (X \ Y) \/ (X \/ Y) by Th28
.= (X \ Y) \/ (X \/ (Y \ X)) by Th67
.= ((X \ Y) \/ (X /\ X)) \/ (Y \ X) by Th28
.= (X \ (Y \ X)) \/ (Y \ X) by Th64
.= X \+\ (Y \ X) by Th78 ; :: thesis: verum