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

now

let i be set ; :: thesis: ( i in I implies (X \ Z) . i c= (Y \ Z) . i )
assume A2: i in I ; :: thesis: (X \ Z) . i c= (Y \ Z) . i
then A3: ( (X \ Z) . i = (X . i) \ (Z . i) & (Y \ Z) . i = (Y . i) \ (Z . i) ) by Def9;
X . i c= Y . i by A1, A2, Def5;
hence (X \ Z) . i c= (Y \ Z) . i by A3, XBOOLE_1:33; :: thesis: verum

end;

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