Proof of a basic $AC_\omega$ equivalence On Wikipedia it is mentioned that "...  in order to prove that every accumulation point $x$ of a set $S\subseteq \mathbf R$ is the limit of some sequence of elements of $S\setminus \{x\}$, one uses (a weak form of) the axiom of countable choice. When formulated for accumulation points of arbitrary metric spaces, the statement becomes equivalent to $AC_\omega$. ..."
I have Herrlich's paper "Choice principles in elementary topology and analysis" where in theorem 2.4. it is stated that these are indeed equivalent. Then I looked up the reference he quotes, [4], which are Bentley H.L., Herrlich H., Countable choice and pseudometric spaces which does not contain the proof and [14] Herrlich H., Steprans J., Maximal filters, continuity and choice principles. does also not contain the proof, hence my question: 
Where can I see a proof of 

"if $S$ is a set in a metric space $X$ with accumulation point $s$
  then there exists a sequence $s_n$ in $S$ converging to $s$"
  $\implies$ $AC_\omega$

? (the other implication is clear to me). Thanks.     
 A: The proof does appear in Herrlich and Steprans paper. It is the combination of propositions 4 and 5.
The first step is to prove that $\sf AC_\omega$ is equivalent to the following statement:

For each sequence of non-empty sets $(X_n)$ there exists a strictly monotone function $\sigma\colon\Bbb{N\to N}$ with $\prod\limits_{n\in\Bbb N}X_{\sigma(n)}\neq\varnothing$.

Obviously $\sf AC_\omega$ implies this condition, to see the reverse implication, suppose this statement is true, take $A_n=\prod\limits_{i=0}^n X_n$, these are non-empty sets. And the $\sigma$ which exists witnessing $\prod_{n\in\Bbb N}A_{\sigma(n)}$ defines a choice from $X_n$'s, by taking $(a_n)$ where $a_n\in A_{\sigma(n)}$, then $a_n=(x_0^n,\ldots,x_{\sigma(n)}^n)$. Since $n\leq\sigma(n)$ for all $n$, we can safely define the sequence $(x_n^n)$ as a choice from the $X_n$'s. $\square$
The second proposition is this:

Proposition 5. The following conditions are equivalent:
  
  
*
  
*$\sf AC_\omega$.
  
*For each metric space $A$, the following are equivalent:
  
*
  
*$x$ is an accumulation point of $A$.
  
*There exists a sequence $(a_n)$ in $A$ with $a_n\to x$.
  
  
*For mappings $f$ between metric spaces the following are equivalent:
  
*
  
*$f$ is continuous.
  
*$f$ is sequentially continuous.
  
  

Clearly $\sf AC_\omega$ implies the other two equivalences. And they are equivalent themselves, (3) implies (2) by taking the identity function, and (2) implies (3) because the failure of (3) is really just the failure of (2).
So we only have to show that (2) implies $\sf AC_\omega$. This is done as follows, take $(X_n)$ to be a sequence of non-empty sets, let $X$ be the following set, $$X=\{\infty\}\cup\bigcup_{n\in\Bbb N}\Big(X_n\times\{n+1\}\Big),$$
along with the metric:
$$d\Big(\langle x,n\rangle,\langle y,m\rangle\Big)=\begin{cases}\frac1n & n=m\\\left|\frac1n-\frac1m\right|& n\neq m\end{cases}\\
d\Big(\langle x,n\rangle,\infty\Big)=d\Big(\infty,\langle x,n\rangle\Big)=\frac1n\\
d(\infty,\infty)=0$$
Since $\infty$ is clearly an accumulation point of $A=X\setminus\{\infty\}$, by our assumption there is a sequence $a_n\to\infty$, and we may assume without loss of generality that this sequence is strictly decreasing (in its distances that is). Let $\sigma$ be the unique function such that $a_n\in X_{\sigma(n)}\times\{\sigma(n)+1\}$. This clearly defines a partial choice as in the previous proposition, so $\sf AC_\omega$ holds. $\square$
