Sets in constructive mathematics It is not completely clear how Bridges, Richman and Youchuan treated sets in their paper. Example is in the following lemma (Lemma 7 on p. 7):

Let $U$ and $V$ be (inhabited to mean $\exists u \in U, \exists v \in V$) sets of a Banach space such that $U \cup V$ is dense. Then,
the following holds:

*

*If $u_0 \in U$ and $v_0 \in V$, then $\rho([u_0, v_0], \bar U \cap \bar V) = 0$

*$\rho(x, \bar U \cap \bar V) = \rho(x, U) \wedge \rho(x, V)$
...
To do this, choose $w$ in $U \cup V$ within ...

If a set $X$ is inhabited, then there is (at least) one point that can be constructed. How can other points be constructed?
 A: Suppose we know that there exists $x \in A$ such that $\phi(x)$, and we want to prove $\psi$. Then the elimination rule for existential quantifiers allows us to argue as follows:

We know that $\exists x \in A . \phi(x)$, and so we may assume to have $a \in A$ such that $\phi(a)$. [Insert argument using $a$ and the fact that $\phi(a)$ here.] Therefore $\psi$, as required.

There is a technical condition, namely that $a$ must not appear in $\psi$. This is precisely how we always use knowledge that something exists. Many authors use the word "choose", as follows:

We know that $\exists x \in A . \phi(x)$, and so choose $a \in A$ such that $\phi(a)$. [Insert argument using $a$ and the fact that $\phi(a)$ here.] Therefore $\psi$, as required.

This has nothing to do with choice! It is still just elimination of existential quantifiers, but the word "choose" confuses many into thinking we're applying the axiom of choice.
All of the above holds equally well classically and constructively. But people worry about constructive math, as if somehow there existence is more special, so let me address this as well. If we have the assumption $\exists x \in A . \phi(x)$ then we need not "construct" an element $a \in A$ such that $\phi(x)$. The assumption gives us some $a \in A$ such that $\phi(a)$. We do not know which $a$ it gives us, but it gives us one. We are thus allowed to use such an $a \in A$, keeping in mind that all we know about it is $\phi(a)$.
Let us apply this to density. Suppose you know that $U \cup V$ is dense in $A$. The definition of density is: for every $\epsilon > 0$ and $x \in A$ there exists $y \in U \cup V$ such that $d(x,y) < \epsilon$. So, given $x_0 \in A$ and $\epsilon_0 > 0$, we may conclude that there exists $y \in U \cup V$ such that $d(x_0, y) < \epsilon_0$. Therefore, we may say: there is $a \in U \cup V$ such that $d(x_0, a) < \epsilon_0$. There is no need to "construct" $a$. The fact that $a$ is there is precisely the existential assumption!
A: The lemma has an existence hypothesis; it is this existence hypothesis that allows the proof to “choose” a point when necessary.
$\newcommand{\x}{\vec{x}}$Specifically, the lemma assumes that $U \cup V$ is dense.  That says (by definition) that for every suitable $x$ and $\varepsilon$, there exists some point in $U \cup V$  within $\epsilon$ of $x$.
But then the logical rules for the existential quantifier tell us: if we’re trying to prove some goal, and we have established that there exists some object with some property, it suffices to prove the goal assuming that we have some specific object with that property.
Formally, this is the natural deduction rule that says: If $\Gamma,\, \varphi(\x, y) \vdash \psi(\x)$, then $\Gamma,\, \exists y. \varphi(\x, y)\vdash \psi(\x)$ (where $y$ is not free in $\Gamma$ or $\psi(\x)$).
(Most other formalisations of constructive logic have some similar rule or axiom.)  But in prose, it is often phrased as e.g. “We know there exists some $y$ such that […].  So, choose some such $y$; then …”
So the proof is not “constructing” some new point in the sense which — as you say — would be impossible in general.  It is just choosing (for the purpose of the proof in question) points whose existence is guaranteed by the assumption that $U \cup V$ is dense.
