Nested intervals plus the Archimedean property imply Bolzano-Weierstrass, by repeated bisection

Since $M_0 \ge |x_0| \ge 0$, the element $M := M_0 + 1_F$ satisfies $M > 0$ and $|x_k| \le M_0 < M$ for every $k$, so $-M \le x_k \le M$ and $x_k \in [-M, M]_F$ for every $k$.

Writing $m(a,b) := (a + b) \cdot (2 \cdot 1_F)^{-1}$, define $f : F \times F \to F \times F$ by $f(a,b) := (a, m(a,b))$ when $a \le b$ and the set of $k$ with $x_k \in [a, m(a,b)]_F$ is cofinal, and $f(a,b) := (m(a,b), b)$ otherwise; the recursion theorem applied to $F \times F$, the element $(-M, M)$ and $f$ gives a unique $g : \mathbb{N} \to F \times F$ with $g(0) = (-M, M)$ and $g(n+1) = f(g(n))$, and we write $g(n) = (a_n, b_n)$ and $I_n := [a_n, b_n]_F$.

By induction on $n$, all of the following hold: $a_n \le b_n$; $b_n - a_n = 2M \cdot ((2 \cdot 1_F)^n)^{-1}$; $I_{n+1} \subseteq I_n$; and the set $E_n := \{\, k : x_k \in I_n \,\}$ is cofinal. For $n = 0$ this is step 1.1 together with $b_0 - a_0 = 2M$ and $(2 \cdot 1_F)^0 = 1_F$. For the step, put $m := m(a_n,b_n)$, so that $a_n \le m \le b_n$ and $m - a_n = b_n - m = (b_n - a_n) \cdot (2 \cdot 1_F)^{-1}$; if the first clause of $f$ applies then $I_{n+1} = [a_n, m]_F$ has the four properties by construction, and otherwise there is $K$ with $x_k \notin [a_n, m]_F$ for all $k \ge K$, so every $k \ge K$ in the cofinal set $E_n$ has $m < x_k \le b_n$ and hence lies in $\{k : x_k \in [m, b_n]_F\}$, which is therefore cofinal as well.

The lengths $b_n - a_n$ tend to $0$ in $F$: given $\varepsilon > 0$, the element $2M \varepsilon^{-1}$ is positive, so [L3] supplies $n \ge 1$ with $2M\varepsilon^{-1} < n \cdot 1_F$, and then for every $p \ge n$ Bernoulli at $x = 1_F$ gives $(2 \cdot 1_F)^p \ge 1_F + p \cdot 1_F > p \cdot 1_F \ge n \cdot 1_F > 2M\varepsilon^{-1} > 0$, whence $((2 \cdot 1_F)^p)^{-1} < \varepsilon (2M)^{-1}$ and $b_p - a_p = 2M \cdot ((2 \cdot 1_F)^p)^{-1} < \varepsilon$.

Since each $E_j$ is cofinal, for every $j$ and every $n$ the set $\{\, k \in \mathbb{N} : k > n \text{ and } x_k \in I_{j+1} \,\}$ is nonempty and so has a least element; the recursion theorem applied to $\mathbb{N} \times \mathbb{N}$, the element $(0,0)$ and the map sending $(j,n)$ to $(j+1, \min\{k : k > n, \ x_k \in I_{j+1}\})$ therefore yields indices $n_0 = 0$ and $n_{j+1} = \min\{k : k > n_j, \ x_k \in I_{j+1}\}$.

The sequence $(I_n)$ is nested with lengths tending to $0$, so (NIP) supplies an element $c$ lying in $I_n$ for every $n$.

Since $n_{j} < n_{j+1}$ for every $j$, the map $j \mapsto n_j$ is strictly increasing and $(x_{n_j})$ is a subsequence of $(x_k)$; moreover $x_{n_j} \in I_j$ for every $j$, the case $j = 0$ being $x_0 \in I_0$ from step 1.1.

For every $j$, both $x_{n_j}$ and $c$ lie in $I_j$, so $x_{n_j} - c \le b_j - a_j$ and $c - x_{n_j} \le b_j - a_j$, whence $|x_{n_j} - c| \le b_j - a_j$.

Given $\varepsilon > 0$ in $F$, step 3.1 supplies $J$ with $b_j - a_j < \varepsilon$ for all $j \ge J$, so $|x_{n_j} - c| < \varepsilon$ for all $j \ge J$; hence $x_{n_j} \to c$ in $F$.

An arbitrary bounded sequence in $F$ has therefore been given a subsequence converging in $F$, so $F$ has (BW).