Solution (source code)

= Solution

Here is a nested-interval proof of the <Bolzano-Weierstrass theorem>. Put every term of the bounded real <sequence> in a <closed interval> $I_0=[-M,M]$, with $M>0$. Bisect this interval and choose a closed half containing infinitely many terms. Repeating gives nested <closed intervals> $I_j=[l_j,r_j]$, each containing infinitely many <sequence> terms, with length $2M/2^j$.

By the <least-upper-bound property>, $x_* =\sup_j l_j$ exists. For each $j$, every lower endpoint lies at most $r_j$, while $l_j\le x_*$; hence $x_*\in I_j$. Choose increasing indices $n_j$ with $a_{n_j}\in I_j$, possible because each interval contains infinitely many terms. Then
$$
|a_{n_j}-x_*|\le 2M/2^j\longrightarrow0.
$$
Thus \b[every bounded real <sequence> has a <convergent subsequence>].

For a <sequence> with no <convergent subsequence>, take $a_n=n$: any <subsequence> has $n_j\ge j$, so its terms tend to positive infinity rather than to a finite <limit of a sequence>. For an unbounded <sequence> with a <convergent subsequence>, take $a_{2n}=0$ and $a_{2n-1}=n$. Its odd terms are unbounded, while its even <subsequence> converges to zero.