Can the following sequence be shown to necessarily exist w/o AoC? Considering any proper subset $S$ of the real numbers that is bounded above and contains infinitely many elements, $S$ necessarily contains a non-decreasing sequence $(s_n)$ with the following property:
$$\forall \alpha \in S, \exists n \in \mathbb{N} \textrm{ such that $\alpha \leq s_n$}?$$
PROOF
Note: By $(s_n) \subset S,$ I mean a sequence $(s_n)$ that is fully contained in the set $S.$ Excuse this notation if it is improper.
Suppose
$$\exists \alpha \in S \text{ such that } \forall (s_n) \subset S \textrm{ it follows that } \alpha > s_n, \forall n \in \mathbb{N}.$$
There is an immediate contradiction, for consider any sequence $(s_n)$ such that for some $N \in \mathbb{N}$ $$\forall n \geq N, s_n = \alpha.$$
Hence, $\forall \alpha \in S,$ if $\alpha > s_n, \forall n \in \mathbb{N},$ $\forall (s_n) \subset S \rightarrow$ contradiction. Hence, there necessarily exists such a sequence.

Does this proof employ bad reasoning? If so, where?
 A: Your argument is impermissibly switching around quantifiers. You want to prove
$$ \tag{1} \exists (s_n)\; \forall \alpha \; \exists n : s_n \ge \alpha $$
If you want to do that by an indirect proof, you need to start by assuming the negation of this, which is
$$ \tag{2} \forall (s_n) \; \exists \alpha \; \forall n : s_n < \alpha $$
But what you're actually assuming is something different, namely
$$ \tag{3} \exists \alpha \; \forall (s_n) \; \forall n : s_n < \alpha $$
But (3) is a stronger assumption than (2) -- it says you can find an $\alpha$ that does not depend on $(s_n)$, which the $\alpha$ in (2) is allowed to. Therefore (3) is a stronger assumption than the one an indirect proof allows you to make.
As a concrete example of (3) being stronger, note that if we let $\alpha$ and the $s_i$s range over $\omega_1$ (with its natural ordering) instead of a subset of $\mathbb R$, then (2) becomes true, whereas (3) is false.

I don't know if your claim can be proved without the axiom of choice. Intuitively I think it has the feeling of something that might well require choice.
You don't need much choice, as those things go, though. Countable choice (which is a quite weak choice principle) will easily do.
