Distance from a Point to a Nonempty Subset of a Metric Space

In the setting of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces and Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $(X,d)$ be a metric space, let $A\subseteq X$ be nonempty, and let $x\in X$.

(i) Distance to a subset. The distance from $x$ to $A$ is the infimum in $\mathbb{R}$

$$\operatorname{dist}(x,A)=\inf\{d(x,a):a\in A\}$$

(it exists by The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (viii), the set being nonempty and bounded below by $0$ by Metric Space (ii)).