Perfect subsequence lemma ($x_{i_0}\le x_{i_1}\le \cdots$)

Every infinite sequence in a well-quasi-ordering has an infinite subsequence all of whose earlier terms precede its later terms. Some term must have infinitely many later terms above it: otherwise choose each new index outside the finitely many upper-cone index sets of the terms already chosen, producing a bad sequence. Apply the same observation successively inside the infinite upper-cone subsequence. Each restriction preserves all earlier inequalities, proving the assertion.