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