Product Metric on the Cartesian Product of Two Metric Spaces

Let $(X,d_X)$ and $(Y,d_Y)$ be metric spaces, and let $X\times Y$ be the Cartesian product of the sets $X$ and $Y$. Let $\mathbb{R}$ be the set of real numbers with the order $\le$ of its ordered field structure, which is in particular a total order.

The product metric on $X\times Y$ is the function

whose value at a pair of points $(x_1,y_1),(x_2,y_2)\in X\times Y$ is the maximum