We prove the assertion for left options; the right-option proof is its mirror. Use the one-game induction scheme of Definition 2.6. Let \(x\) be surreal, and let \(x^L\) be a left option. By Definition 2.9, \(x^L\) is itself surreal. We verify the two clauses of Definition 2.4 for \(x^L\preceq x\).

Let \(z\) be a left option of \(x^L\), and suppose \(x\preceq z\). Since \(\operatorname {bd}(x^L){\lt}\operatorname {bd}(x)\) by Lemma 2.3, the induction hypothesis applied to the surreal game \(x^L\) gives \(z\preceq x^L\). But the left-option clause of \(x\preceq z\), applied to the option \(x^L\) of \(x\), forbids \(z\preceq x^L\). Next let \(x^R\) be a right option of \(x\). The separation condition in Definition 2.9 is precisely \(\neg (x^R\preceq x^L)\). Hence \(x^L\preceq x\).

It remains to exclude the reverse comparison. If \(x\preceq x^L\), its left-option clause gives \(\neg (x^L\preceq x^L)\), contradicting reflexivity from Theorem 2.7. Thus \(x^L\prec x\) by Definition 2.4. The mirrored argument proves \(x\prec x^R\) for every right option \(x^R\).

Suppose \(\neg (x\preceq y)\). Negating the two universal clauses in Definition 2.4 produces one of two witnesses: either there is a left option \(x^L\) such that \(y\preceq x^L\), or there is a right option \(y^R\) such that \(y^R\preceq x\). In the first case, Theorem 2.10 gives \(x^L\preceq x\); in the second it gives \(y\preceq y^R\). Transitivity from Theorem 2.7 therefore yields \(y\preceq x\) in either case. Hence

which proves totality.

For trichotomy, choose a direction supplied by totality and then distinguish whether the reverse weak comparison also holds. If both hold, then \(x\sim y\); if exactly one holds, then the corresponding comparison is strict. These are precisely the definitions in Definitions 2.4 and 2.5.