let I be set ; :: thesis: for X, Y being ManySortedSet of I st X misses Y holds
(X \/ Y) \ Y = X
let X, Y be ManySortedSet of I; :: thesis: ( X misses Y implies (X \/ Y) \ Y = X )
(X \/ Y) \ Y = X \ Y by Th81;
hence ( X misses Y implies (X \/ Y) \ Y = X ) by Th126; :: thesis: verum