The Absolute Value Metric on the Real Line

Let $\mathbb{R}$ be the set of real numbers, with the addition and multiplication and the order $\le$ of its ordered field structure, and let $|\cdot|$ be the absolute value on $\mathbb{R}$. For $s,t\in\mathbb{R}$ write $s-t$ for $s+(-t)$.

Let $d_{\mathbb{R}}:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ be the function given by

Then $d_{\mathbb{R}}$ is a metric on $\mathbb{R}$. We call the metric space $(\mathbb{R},d_{\mathbb{R}})$ the real line.