First show that \(0\prec y\) forces a left option \(y^L\) with \(0\preceq y^L\). If no left option had this property, the left clause in Definition 2.4 would give \(y\preceq 0\); the other clause is vacuous because \(0\) has no right options. This contradicts the strict hypothesis.

Proceed by the well-founded scheme of Definition 2.6, using Lemma 2.3, and choose such a \(y^L\). By Definition 2.9, the option \(y^L\) is surreal. Split according as \(y^L\preceq 0\). If it does, then the two weak comparisons give \(y^L\sim 0\). Theorem 4.11, together with the commutativity and zero-product laws in Theorem 4.2, gives \(xy^L\sim 0\), hence \(0\preceq xy^L\). Otherwise Definition 2.4, together with the already known comparison \(0\preceq y^L\), gives \(0\prec y^L\). Since \(y^L\) has smaller birthday, the induction hypothesis gives \(0\prec xy^L\), and therefore again \(0\preceq xy^L\).

Apply Theorem 4.12 to \(0\prec x\), with common surreal factor \(y\) and left option \(y^L\). Simplifying its left cross inequality by the zero-product laws of Theorem 4.2 and the zero-sum laws of Theorem 3.2 yields \(xy^L\prec xy\). The mixed transitivity assertion of Theorem 2.7, applied to \(0\preceq xy^L\prec xy\), proves \(0\prec xy\).

For strict positivity, choose surreal representatives \(a_0,b_0\) of the two classes using Definition 3.10. The hypotheses become \(0\prec a_0\) and \(0\prec b_0\). By Theorem 5.6, \(0\prec a_0b_0\); passing to equivalence classes and using Definition 5.2 gives \(0{\lt}ab\).

Suppose only \(0\leq a\) and \(0\leq b\). The linear order of Theorem 3.11 splits each weak comparison into a strict inequality or equality. If both inequalities are strict, the first part of this theorem gives \(0{\lt}ab\), hence \(0\leq ab\). If \(a=0\) or \(b=0\), the appropriate zero-product law in Theorem 5.3 gives \(ab=0\). These cases prove nonnegative-product closure.

Finally, Definitions 2.1 and 2.4 show directly that \(0\preceq 1\): the left-option condition for \(0\) and the right-option condition for \(1\) are both vacuous. Hence their equivalence classes satisfy \(0\leq 1\).

Assume \(b\leq c\) and \(0\leq a\). By Theorem 3.11, the first hypothesis is equivalent to \(0\leq c-b\). The nonnegative-product assertion of Theorem 5.7 gives \(0\leq a(c-b)\), while the ring laws of Theorem 5.5 give \(a(c-b)=ac-ab\). The ordered additive group equivalence \(0\leq ac-ab\Longleftrightarrow ab\leq ac\) yields weak monotonicity on the left. For the right-sided assertion, suppose \(a\leq b\) and \(0\leq c\). Then \(0\leq b-a\), so

and hence \(ac\leq bc\).

If \(b{\lt}c\) and \(0{\lt}a\), use instead \(0{\lt}c-b\). Strict positivity of a product, again by Theorem 5.7, gives \(0{\lt}a(c-b)=ac-ab\), which Theorem 3.11 identifies with \(ab{\lt}ac\). Similarly, \(a{\lt}b\) and \(0{\lt}c\) imply

and hence \(ac{\lt}bc\). These four implications give the four weak and strict, left- and right-sided multiplication-order compatibilities asserted in the theorem.

Theorem 3.11 gives translation invariance of the order, Theorem 5.5 gives the commutative ring laws, and the weak and strict multiplication compatibility assertions are Theorem 5.8. In particular, if \(c+a\leq c+b\), translating both sides by \(-c\) and simplifying with the additive group laws of Theorem 3.11 gives \(a\leq b\). Thus addition reflects order as required.

It remains to supply nontriviality. At game level, \(0\) is the sole left option of \(1\) by Definition 2.1. If \(1\preceq 0\), the left clause of Definition 2.4 would require \(\neg (0\preceq 0)\), contradicting the reflexivity assertion of Theorem 2.7. Therefore \(0\) and \(1\) are not equivalent, so their classes in Definition 3.10 are distinct. Order reflection and the weak and strict multiplication inequalities above establish all the claimed ordered-ring compatibility axioms.

By Theorem 3.11, \(\mathbf{No}_{\mathrm{short}}\) is a linear ordered additive commutative group. By Theorem 5.5, \(\mathbf{No}_{\mathrm{short}}\) is a commutative ring. Theorem 5.9 proves compatibility of these algebraic operations with the linear order. Hence \(\mathbf{No}_{\mathrm{short}}\) is a linear ordered commutative ring.