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 Th75;
hence ( X misses Y implies (X (\/) Y) (\) Y = X ) by Th115; :: thesis: verum