Jonathan, thanks for
>Thus, M× can't be defined independent of any particular order.

I got lost among 3 trees, and all these is tightly bound to what comes next in Lecture 23 and Lecture 24.

Indeed **any** \\(\rho : X \times X \to X\\), where we assume that \\(X\\) is already equipped with order relation \\(\leq_X\\): \\((X, \leq_X)\\), **automatically induces** a natural preorder on \\(X \times X \\) by requiring
\[ \rho(x_1, x_2) \leq_X \rho(x'_1, x'_2) \Rightarrow (x_1, x_2) \leq_\rho (x'_1, x'_2) \]

where \\(\leq_\rho = \leq_{X \times X}\\) is an induced order relation on \\(X \times X \\), making it into preorder: \\((X \times X, \leq_\rho)\\). Since this relation is induced, implication also goes backwards:
\[ (x_1, x_2) \leq_\rho (x'_1, x'_2) \Rightarrow \rho(x_1, x_2) \leq_X \rho(x'_1, x'_2) \]
which is exactly a **monotonicity** condition! So things are starting to fall into their places, at last.

And now we can say that among all possible \\(\rho\\) there indeed exist some functions which additionally support
\[ C^\times: x_1 \le_X x'_1 \textrm{ and } x_2 \le_X x'_2 \Rightarrow \rho(x_1, x_2) \le_\rho \rho(x'_1, x'_2) \]

Okay, now only what I need is to figure out how this condition structures the \\( (X \times X, \leq_\rho) \\) preorder, and how preorders supporting it differ from others.