Under dependent choice, Riesz lemma builds an infinite separated sequence in the unit sphere

Let $S$ be the set of all finite lists $s=(u_0,\dots ,u_m)$ of unit vectors in $X$ such that $\mathrm{\parallel }{u}_j-u_k\mathrm{\parallel }>\alpha$ for all $j\mathrm{\ne }k$. The set $S$ is nonempty because any single unit vector lies in it: choose any nonzero $u\in X$ and normalize it.

Define a relation $R$ on $S$ by $sRt$ when $t$ is obtained from $s$ by appending one more unit vector $u$ with $\mathrm{dist}(u,\mathrm{span}(s))>\alpha$. If $s=(u_0,\dots ,u_m)\in S$, then the finite span $M:=\mathrm{span}(s)$ is generated by a finite list, so by deleting dependent terms one obtains an ordered basis of finite length for $M$. Since $X$ is not the span of any finite list, $M⊊X$; by [L2] it is closed. Now [L3] applies to $M$ and produces a unit vector $u$ with $\mathrm{dist}(u,M)>\alpha$, so $s$ has an $R$-successor. Thus $R$ is entire on $S$.

By [L1], there is a sequence $(s_n{)}_{n\in \mathbb{N}}$ in $S$ with $s_{n}R{s}_{n+1}$ for every $n$. Because each successor appends exactly one new term, the first entries stabilize: if $x_n$ denotes the last entry appended when passing from $s_n$ to $s_{n+1}$, then every earlier $x_j$ remains in all later lists.

For $m<n$, the vector $x_n$ was chosen with $\mathrm{dist}(x_n,\mathrm{span}(x_0,\dots ,x_{n-1}))>\alpha$, and $x_m$ lies in that span. Hence $\mathrm{\parallel }{x}_n-x_m\mathrm{\parallel }>\alpha$. Every $x_n$ is a unit vector by the definition of $R$. Therefore $(x_n{)}_{n\in \mathbb{N}}$ is the required separated sequence.