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

now

let i be set ; :: thesis: ( i in I implies (X \ Y) . i c= X . i )
assume A1: i in I ; :: thesis: (X \ Y) . i c= X . i
(X . i) \ (Y . i) c= X . i ;
hence (X \ Y) . i c= X . i by A1, Def9; :: thesis: verum

end;

hence X \ Y c= X by Def5; :: thesis: verum