A theorem about infinite sequences of numbers

Theorem.  An infinite sequence of (real) numbers contains an infinite monotonic subsequence. (End of Theorem.)

Proof.  Let the sequence be x(i: 0 ≤ i). Element x(i) is "dominant" means (A j: i+1 ≤ j: x(i) ≥ x(j)). We distinguish two cases.

The number of dominant elements is infinite.  In this case the dominant elements form an infinite subsequence, which is monotonic (viz. descending).

The number of dominant elements is finite.  In this case an N exists such that from x(N) onwards, no dominant element occurs, i.e. (A i: i ≥ N: (E j: i+1 ≤ j: x(i) < x(j))). Hence each x(i) with i ≥ N is the starting element of an infinite subsequence that is increasing, and therefore monotonic.

(End of Proof.)

I found this proof last Sunday evening; the day before I had heard the theorem together with the rumour that it might require a fancy proof. Quod non.