Every bounded infinite sequence of real numbers contains a convergent subsequence
Proof:
Let $E$ the infinite set of values of the sequence.
$E$ bounded and infinite $\Rightarrow E$ contains a limit point $x$.
$x$ limit point of $E \Rightarrow \exists n_1 \in \mathbb{N}:|x_{n_1}-x|<1$.
So by induction if $\exists n_k \in \mathbb{N}:|x_{n_k}-x|<\frac{1}{k}$ then $\exists n_{k+1} \in \mathbb{N}:|x_{n_{k+1}}-x|<\frac{1}{k+1}$, otherwise $x$ is not a limit point of $X$.
So, the sequence constructed $\{x_{n_1},x_{n_2},...,x_{n_k},...\}$ converges to $x$.
End Proof.
In the last step So, the sequence constructed... is there the axiom of choice in a hidden form? Otherwise how can I justify the construction of the set $\{x_{n_1},x_{n_2},...,x_{n_k},...\}$?
There is no essential use of choice here. The natural numbers, as you probably know, are well-ordered.
That means that whenever you have to make a choice, you can always choose the one with the least index.
This is a situation that happens often in analysis, mainly because for the most part doing analysis without [at least dependent] choice is borderline self-abusive.
(Do note, by the way that "$E$ contains a limit point" is wrong, and you should say that "$E$ has a limit point" instead.)