Direct proof of Bolzano-Weierstrass using Axiom of Completeness The author of my intro analysis text has an exercise to give a proof of Bolzano-Weierstrass using axiom of completeness directly. 
Let $(a_n)$ be a bounded sequence, and define the set $$S=\{x \in \mathbb{R} : x<a_n \text{ for infinitely many terms } a_n\}.$$
Show that there exists a subsequence $a_{n_k}$ converging to $s = \sup S$. 
I feel I am close. I know that for any $\epsilon > 0$, there must be infinitely many $a_n$ such that $\sup S - \epsilon < a_n < \sup S + \epsilon$. (If there were only finitely many $a_n$ in that interval, then $\sup S + \frac{\epsilon}{2} \in S$, contradicting $\sup S$ as an upper bound.) However, I don't know how to pinpoint a single subsequence $(a_{n_k})$ such that all such elements with $k \geq \text{ some } N$ are in this interval for all $\epsilon$.
 A: Since $(a_n)$ is bounded, $S$ is nonempty and bounded above. So by AoC there exists an upper bound $s=\sup S$.
Consider $s-\frac1k$ and $s+\frac1k$ where k is an arbitrary but fixed natural number. Since any number smaller than $s$ is not an upper bound of $S$, so $\exists (s'\in S)(s-\frac1k < s')$. Observe the property which forms $S$, by transtivity of $<$, $s-\frac1k$ also has the property: $s-\frac1k < a_n$ for infinitely many terms $a_n$. Apply this similar reasoning on $s+\frac1k$ we can see that $s+\frac1k \notin S$, so there are none or only finitely many terms $a_n$ satisfying $1+\frac1k < a_n$, this is the same as saying there are infinite many terms $a_n$ satisfying $a_n \ge 1+\frac1k$. Combine these two parts we get: for all $k\in N$, there are infinitely many terms of $a_n$ satisfying $s-\frac1k < a_n \le s+\frac1k$.
The last statement gave us a hint of how to build a subsequence of $(a_n)$. For every different $k\in N$, we can pick a term from infinitely many terms that satisfy that inequality. For example we can pick $a_{n_1}$ from $\{a_n : s-1<a_n<s+1\}$. After we picked $a_{n_k}$, we only need to satisfy $n_{k+1}>n_k$ to make this is indeed a subsequence, no repeatition or backward happened. (This is always can be done because for every pick we have infinitely many terms in hand)
Then we need to check whether this subsequence $(a_{n_k})$ converges to something. By intuition this should be $\sup S$. To satisfy the inequality $|a_{n_k}-s|<\epsilon$ for every $\epsilon >0$, choose $K>\frac1\epsilon$. If $k\ge K$ then $\frac1k < \epsilon$ which implies $$s-\epsilon < s-\frac1k < a_{n_k} \le s+\frac1k < s+\epsilon$$
So the B-W theorem has been proved using AoC.
