Perfect subsequence lemma (source code)

= Perfect subsequence lemma
{title2=$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.