Every Sequence in a Totally Ordered Set Has a Monotone Subsequence

In the setting of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion, let $\le$ be a total order on a set $X$, and let $(a_{n})$ be a sequence in $X$, with monotone sequences as in Monotone Sequences §monotone and subsequences as in Subsequences §subsequence.

¶ $(a_{n})$ has a subsequence that is nondecreasing or a subsequence that is strictly decreasing.

¶ $(a_{n})$ has a monotone subsequence.