Work in the quotient \(\mathcal G/{\sim }\) of Definition 3.8, equipped with the ordered additive group structure of Theorem 3.9. The hypothesis is

Adding the same class to both sides and rearranging the additive group gives, respectively,

For example, Definition 4.1 gives

Hence the first rearranged inequality is exactly

which is the class-level form of rule (a). The other three lines give rules (b)–(d) in the same way. The argument works for both weak and strict order because translation preserves both in the ordered additive group.

We prove rule (g),

the other strict rules (e), (f), and (h) are analogous. The first hypothesis means

By Theorem 3.9, this is the strict quotient inequality

The two equivalence hypotheses give the class equalities

Substituting them into the strict inequality gives

Reflecting strict order from the quotient yields

which is exactly \(\operatorname {Cross}_{\prec }(a,c;d,e)\).

We prove only the \(LL\) statement. Its hypotheses are

In the quotient \(\mathcal G/{\sim }\), add \(-[a^Ly^L]\) to both sides and use \([by^L]=[ay^L]\). This gives

whose left side is \([\operatorname {M}(a^L,y;a,y^L)]\) by Definition 4.1. The quotient order in Theorem 3.9 therefore gives

The \(RR\), \(LR\), and \(RL\) statements follow from the same quotient rearrangement with their displayed equivalence and cross-inequality hypotheses.

Apply well-founded induction with the goal order of Definition 4.5. The induction hypothesis is available for every \(A\)-, \(B\)-, or \(C\)-assertion whose multiset measure is smaller. The comparisons in that definition justify replacing a coordinate by an option, replacing one birthday by two smaller birthdays, and deleting an unused coordinate.

Consider \(A(x,y)\). By Definition 2.9, it is enough to prove that every option of \(xy\) is surreal and that every left option is strictly below every right option. Definition 4.1 gives the four option families. If \(x'\) and \(y'\) are options of \(x\) and \(y\), respectively, the corresponding option has the form

The smaller assertions \(A(x',y)\), \(A(x,y')\), and \(A(x',y')\) prove that its three product terms are surreal. Closure under addition and negation, Theorem 3.7, then proves the whole expression surreal.

For separation put \(P(u,v)=\operatorname {M}(u,y;x,v)\). By Definition 4.1, a left option of \(xy\) is

and a right option is

Consider first \(P(x^L_1,y^L)\) and \(P(x^L_2,y^R)\). Since the first is a left option and the second is a right option, we need to prove

Theorem 2.11 compares \(x^L_1\) and \(x^L_2\). Also, Theorem 2.10 and strict transitivity from Theorem 2.7 give \(y^L\prec y\prec y^R\), hence \(y^L\prec y^R\). The three possible comparisons of the two left options give

Here is the first branch in detail. Assume \(x^L_1\prec x^L_2\). The smaller assertion \(C(x^L_1,x^L_2,y)\) gives

Substitute \((a,c;d,e;b)=(x^L_1,x^L_2;y^L,y;x)\) in rule (a) of Theorem 4.7. It becomes

For the second step, the smaller assertion \(C(y^L,y^R,x)\), evaluated at the left option \(x^L_2\) of \(x\), gives

Applying rule (e) of Theorem 4.7 gives \(\operatorname {Cross}_{\prec }(x^L_2,x;y^L,y^R)\). Rule (c), now with \((a,c;d,e;b)=(x^L_2,x;y^L,y^R;y)\), gives

Strict transitivity therefore proves the first chain in the display.

If \(x^L_1\sim x^L_2\), the same \(y\)-slot argument first gives \(P(x^L_1,y^L)\prec P(x^L_1,y^R)\). The two smaller assertions \(B(x^L_1,x^L_2,y)\) and \(B(x^L_1,x^L_2,y^R)\) give

Hence, in \(\mathcal{G}/{\sim }\),

Thus \(P(x^L_1,y^R)\sim P(x^L_2,y^R)\), and the strict–weak composition law proves the middle chain.

Finally, assume \(x^L_2\prec x^L_1\). After the same strict \(y\)-slot movement at \(x^L_1\), the smaller assertion \(C(x^L_2,x^L_1,y)\) gives

Rule (b) of Theorem 4.7, with \((a,c;d,e;b)=(x^L_2,x^L_1;y,y^R;x)\), reverses the \(x\)-slot direction and gives

Strict transitivity proves the last chain. All the \(B\)- and \(C\)-assertions just invoked are smaller by the one-to-two birthday replacement in Definition 4.5.

The \(LL\)-versus-\(RL\), \(RR\)-versus-\(LR\), and \(RR\)-versus-\(RL\) comparisons are proved analogously. This proves \(A(x,y)\).

Now consider \(B(a,b,y)\). Assume \(a\sim b\). By Definition 2.4, to prove \(ay\preceq by\) one must rule out \(by\preceq \lambda \) for every left option \(\lambda \) of \(ay\), and rule out \(\rho \preceq ay\) for every right option \(\rho \) of \(by\).

Definition 4.1 gives two kinds of left option of \(ay\):

We must prove \(\lambda _{LL}\prec by\) and \(\lambda _{RR}\prec by\); either strict inequality contains the corresponding conclusion \(\neg (by\preceq \lambda )\).

For \(\lambda _{LL}\), the smaller assertion \(B(a,b,y^L)\) gives

The comparison \(a^L\prec a\), together with \(a\preceq b\) from \(a\sim b\), gives \(a^L\prec b\). Hence the smaller assertion \(C(a^L,b,y)\) gives the explicit cross inequality

These are exactly the two hypotheses of the \(LL\) implication in Lemma 4.8, so

For \(\lambda _{RR}\), the smaller assertion \(B(a,b,y^R)\) gives

Now \(b\preceq a\) follows from \(a\sim b\), while \(a\prec a^R\); hence \(b\prec a^R\). The smaller assertion \(C(b,a^R,y)\) therefore gives

The \(RR\) implication in Lemma 4.8 now yields

Every assertion used here is smaller by Definition 4.5 and Lemma 2.3.

The two right-option cases are analogous. Explicitly, for the two right options of \(by\), one must prove

These follow analogously from the \(LR\) and \(RL\) implications of Lemma 4.8. The four exclusions prove \(ay\preceq by\).

Interchanging \(a\) and \(b\) gives \(by\preceq ay\). This does not invoke the induction hypothesis at the unchanged measure: the equality

from Definition 4.5 identifies the two collections of strictly smaller assertions, and symmetry of \(a\sim b\) permits the same one-sided proof to be reused. The two weak inequalities are exactly \(ay\sim by\) by Definition 2.5.

Finally consider \(C(x_1,x_2,y)\), with \(x_1\prec x_2\). The assertion to be proved is that, for every left option \(y^L\) and right option \(y^R\) of \(y\),

Unfolding Definition 2.4 gives the following bridge alternative: either a right option \(x_1^R\) satisfies \(x_1^R\preceq x_2\), or a left option \(x_2^L\) satisfies \(x_1\preceq x_2^L\). Indeed, if neither existed, the two universal clauses in that definition would give \(x_2\preceq x_1\), contradicting \(x_1\prec x_2\).

Suppose first that \(x_1^R\preceq x_2\). The smaller assertion \(A(x_1,y)\) makes \(x_1y\) surreal. Its product options are those of Definition 4.1. For each left option \(y^L\) of \(y\), the \(RL\) product option lies above \(x_1y\), so

Work in the quotient of Definition 3.8, whose ordered additive group structure is given by Theorem 3.9. Adding \([x_1^Ry^L]\) gives

Reflection of strict order from the quotient gives

Similarly, for a right option \(y^R\), the \(RR\) product option lies below \(x_1y\):

Adding \([x_1^Ry^R]\) and reflecting strict order gives

These are called the adjacent conditions because their two endpoints are \(x_1\) and its option \(x_1^R\). The required conditions displayed above have endpoints \(x_1,x_2\), so it remains to move the second endpoint from \(x_1^R\) to \(x_2\).

By Theorem 2.11, either \(x_1^R\prec x_2\), \(x_1^R\sim x_2\), or \(x_2\prec x_1^R\). If \(x_1^R\prec x_2\), the smaller assertion \(C(x_1^R,x_2,y)\) supplies

Rule (f) of Theorem 4.7 now composes

The results are precisely \(C_L(x_1,x_2;y,y^L)\) and \(C_R(x_1,x_2;y,y^R)\).

If \(x_1^R\sim x_2\), the smaller \(B\)-assertions give

Replacing these three products in the two adjacent inequalities gives, respectively,

which are again the two required conditions. The remaining alternative \(x_2\prec x_1^R\) contradicts \(x_1^R\preceq x_2\).

The alternative \(x_1\preceq x_2^L\) is analogous, using the adjacent conditions for \(x_2^L,x_2\) and then moving the first endpoint from \(x_2^L\) to \(x_1\).

Apply the \(A(x,y)\) clause of Theorem 4.9 to the two surrealness hypotheses. Its conclusion is precisely that \(xy\) is surreal.

Apply the \(B(x_1,x_2,y)\) clause of Theorem 4.9, with the three surrealness hypotheses and \(x_1\sim x_2\). The conclusion is \(x_1y\sim x_2y\).

Apply the \(C(x_1,x_2,y)\) clause of Theorem 4.9, with the three surrealness hypotheses and \(x_1\prec x_2\). Its two conclusions are precisely the required left and right cross inequalities.