The Distance on the Real Numbers Is a Map with Values the Absolute Differences

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, let $d_{\mathbb{R}}$ be the distance on $\mathbb{R}$, with the difference $s-t$ and the absolute value $|s-t|$ for $s,t\in\mathbb{R}$.

¶ There is exactly one map $f:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ with $f(s,t)=|s-t|$ for all $s,t\in\mathbb{R}$, and it is the distance $d_{\mathbb{R}}$.

¶ For all sets $s$, $t$ and $z$: $((s,t),z)\in d_{\mathbb{R}}$ if and only if $s\in\mathbb{R}$, $t\in\mathbb{R}$ and $z=|s-t|$.