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