let I be set ; :: thesis: for X, Y being ManySortedSet of st X misses Y holds
X \ Y = X
let X, Y be ManySortedSet of ; :: thesis: ( X misses Y implies X \ Y = X )
assume A1: X misses Y ; :: thesis: X \ Y = X

now

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

end;

then ( ( for i being set st i in I holds
(X \ Y) . i = X . i ) & ( for i being set st i in I holds
(Y \ X) . i = Y . i ) ) ;
hence X \ Y = X by Th3; :: thesis: verum