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