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

now

let i be set ; :: thesis: ( i in I implies Y . i misses (X \ Y) . i )
assume i in I ; :: thesis: Y . i misses (X \ Y) . i
then (X \ Y) . i = (X . i) \ (Y . i) by Def9;
hence Y . i misses (X \ Y) . i by XBOOLE_1:79; :: thesis: verum

end;

hence Y misses X \ Y by Def11; :: thesis: verum