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 :: thesis: for i being object st i in I holds
(Z (\) Y) . i c= (Z (\) X) . i

let i be object ; :: 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 Def6;
X . i c= Y . i by A1, A2;
hence (Z (\) Y) . i c= (Z (\) X) . i by A3, XBOOLE_1:34; :: thesis: verum

end;

hence Z (\) Y c= Z (\) X ; :: thesis: verum