let I be set ; :: thesis: for X, Y being ManySortedSet of I holds (X \/ Y) \ Y = X \ Y
let X, Y be ManySortedSet of I; :: thesis: (X \/ Y) \ Y = X \ Y
thus (X \/ Y) \ Y = (X \ Y) \/ (Y \ Y) by Th72
.= (X \ Y) \/ ([[0]] I) by Th52
.= X \ Y by Th22, Th43 ; :: thesis: verum