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