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

now

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

end;

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