I'm trying to see if the following proof use any kind of choice beyond the choices ZF allows: Assume nested intervals theorem on real numbers. So shortly, if $I_n$ is a sequence of nested intervals whose length converges to $0$ (with closed intervals on R), then intersection of all of them is a singleton.
We want to show that every non-empty subset of R which is bounded from above has a supremum.
Now, let $A \subset$ R and let $a \in A$ and $r \in$ R be an upper bound for the set $A$. Now our first interval is $[a,r]$. If there is no element in $A$, which is bigger than $a$, then we are done and likewise, if there is no real number less than $r$ which is an upper bound, then we are done. So we can choose this two new numbers and build another interval.
Now, writing this proof here, I noticed that the length doesn't have to go to $0$, so this proof is not correct. I don't ask a correct proof, which would be I am sure a duplicate. I am asking if the process above requires AC or something alike.
You can always choose these numbers to be rational numbers, since the rational numbers are dense in every non-singleton interval.
Since the rational numbers are countable, we can prove there is a nice choice function from the non-empty sets of rational numbers, so no choice is actually needed.