Here is a question from Munkres Topology:
and here is its solution:
I think that while choosing $b_1,b_2,\dots$ we are using Axiom of Choice. But again, since for each $b_n$ we are 'choosing' only one element from a nonempty set, I think we do not have to apply Axiom of Choice.
I am confused!
Regarding your comment on the other answer, choosing $b_1\in B$ does not require Choice. By hypothesis, $B\neq \varnothing$, and so we may let $b_1\in B$. This can consequently be done any finite number of times given finitely many nonempty sets. It's only once you have infinitely many sets that you need Choice.
As the original question is stated, though, Munkres' proof does use Choice. It actually only requires a weakened form of Choice known as Dependent Choice (DC), which states that given a nonempty set $X$ and a relation $R$ on $X$ such that $(\forall x\in X)(\exists y\in x)(x\, R \, y)$, there exists a sequence $x_1,x_2,...$ of elements of $X$ such that for each $n\in \mathbb N$ we have $x_n\, R\, x_{n+1}$.
In the proof in the OP, since $B$ is unbounded below, the relation $>$ on $B$ satisfies the necessary hypothesis for DC. Consequently, by DC, there exists a sequence $b_1,b_2,...$ of elements of $B$ such that for each $n\in\mathbb N$, we have $b_n > b_{n+1}$.
Since the integers are countable, we can enumerate them as use that as a choice. But for the negative integers it's even simpler. Just go down the order of the integers.
For a general linear order, though, this would require some choice. So you are right to be skeptical.
Do note, though, that just choosing one element from a set can be misleading. If you end up potentially choosing from infinitely many sets (each choice requires you that the next choice is from a smaller set) then the axiom of choice might still be necessary.
