Solution (source code)

= Solution

Call an index $n$ a peak if $a_n\geq a_m$ for every $m>n$. If there are infinitely many peaks, list their indices increasingly. Each selected value is at least every later selected value, so this gives a nonincreasing <subsequence>.

If there are only finitely many peaks, choose an index beyond the last one. Every index from then onward has a later index with strictly larger value. Select these recursively: $n_{j+1}>n_j$ with $a_{n_{j+1}}>a_{n_j}$. This gives an increasing <subsequence>. Neither <complex argument> requires the original <sequence> to be bounded. \b[Every real <sequence> therefore has a monotone <subsequence>], as asserted by the <monotone subsequence theorem>.