let I be set ; :: thesis: for X, Y being ManySortedSet of I holds X (/\) Y misses X (\+\) Y
let X, Y be ManySortedSet of I; :: thesis: X (/\) Y misses X (\+\) Y

now :: thesis: for i being object st i in I holds
(X (/\) Y) . i misses (X (\+\) Y) . i

let i be object ; :: thesis: ( i in I implies (X (/\) Y) . i misses (X (\+\) Y) . i )
assume i in I ; :: thesis: (X (/\) Y) . i misses (X (\+\) Y) . i
then ( (X (/\) Y) . i = (X . i) /\ (Y . i) & (X (\+\) Y) . i = (X . i) \+\ (Y . i) ) by Def5, Th4;
hence (X (/\) Y) . i misses (X (\+\) Y) . i by XBOOLE_1:103; :: thesis: verum

end;

hence X (/\) Y misses X (\+\) Y ; :: thesis: verum