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

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

end;

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