Solution (source code)

= Solution
{c}

For a nonempty <set> $A\subseteq\mathbb R$, a <supremum> is a <real number> $s$ such that $a\leq s$ for every $a\in A$, and every <upper bound> $u$ of $A$ satisfies $s\leq u$. Equivalently, $s$ is an <upper bound> and, for every $\varepsilon>0$, some $a\in A$ satisfies $a>s-\varepsilon$. By <completeness of the real numbers>, it exists whenever $A$ is nonempty and bounded above.

An increasing <monotone sequence> satisfies $a_{n+1}\geq a_n$ for every $n$; a <bounded sequence> satisfies $|a_n|\leq M$ for some finite $M$ and every $n$. Put $s=\sup\{a_n:n\geq1\}$. Given $\varepsilon>0$, the defining property of the <supremum> supplies $N$ with $a_N>s-\varepsilon$. For every $n\geq N$, <monotonicity> gives
$$
s-\varepsilon<a_N\leq a_n\leq s.
$$
This is exactly the definition of <convergent sequence>, so the <bounded monotone sequence theorem> gives $\boxed{a_n\to s}$.