That is, for every infinite sequence of totally-ordered countable sets, there exists an order embedding from an earlier member of the sequence to a later member.
More generally, Laver proved the same result for order embeddings of countable unions of scattered orders.
[2][3] In reverse mathematics, the version of the theorem for countable orders is denoted FRA (for Fraïssé) and the version for countable unions of scattered orders is denoted LAV (for Laver).
[4] In terms of the "big five" systems of second-order arithmetic, FRA is known to fall in strength somewhere between the strongest two systems,
However, it remains open whether it is equivalent to ATR0 or strictly between these two systems in strength.