[proofplan] We use quantifier elimination for real closed ordered fields to replace an arbitrary formula by a quantifier-free formula equivalent in every real closed ordered field. It remains to show that quantifier-free formulas have the same truth value in $K$ and $L$ on tuples from $K$. This follows because terms evaluate identically under the inclusion $K \subset L$, and atomic equalities and inequalities are reflected by the field and order substructure relation. [/proofplan] [step:Replace the given formula by a quantifier-free equivalent modulo $\operatorname{RCF}$] Fix an integer $m \geq 1$, an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x_1,\dots,x_m)$, and a tuple $a = (a_1,\dots,a_m) \in K^m$. By the quantifier elimination theorem for real closed ordered fields (citing a result not yet in the wiki: Quantifier Elimination for Real Closed Fields), there exists a quantifier-free $\mathcal{L}_{\mathrm{or}}$-formula $\psi(x_1,\dots,x_m)$ such that \begin{align*} \operatorname{RCF} \models \forall x_1 \cdots \forall x_m \, \bigl(\varphi(x_1,\dots,x_m) \leftrightarrow \psi(x_1,\dots,x_m)\bigr). \end{align*} Since $K \models \operatorname{RCF}$ and $L \models \operatorname{RCF}$, we have \begin{align*} K \models \varphi(a_1,\dots,a_m) &\Longleftrightarrow K \models \psi(a_1,\dots,a_m), \\ L \models \varphi(a_1,\dots,a_m) &\Longleftrightarrow L \models \psi(a_1,\dots,a_m). \end{align*} Thus it suffices to prove that $K$ and $L$ agree on the quantifier-free formula $\psi$ at the tuple $a$. [guided] Fix an integer $m \geq 1$, an $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x_1,\dots,x_m)$, and a tuple $a = (a_1,\dots,a_m) \in K^m$. The obstacle is that $\varphi$ may contain quantifiers over the ambient field, so a direct comparison between $K$ and $L$ would have to compare two different domains of quantification. Quantifier elimination removes that obstacle. By the quantifier elimination theorem for real closed ordered fields (citing a result not yet in the wiki: Quantifier Elimination for Real Closed Fields), there is a quantifier-free $\mathcal{L}_{\mathrm{or}}$-formula $\psi(x_1,\dots,x_m)$ such that every real closed ordered field satisfies \begin{align*} \forall x_1 \cdots \forall x_m \, \bigl(\varphi(x_1,\dots,x_m) \leftrightarrow \psi(x_1,\dots,x_m)\bigr). \end{align*} Because both $K$ and $L$ are models of $\operatorname{RCF}$, this equivalence is valid inside both structures. Evaluating at the tuple $a \in K^m \subset L^m$ gives \begin{align*} K \models \varphi(a_1,\dots,a_m) &\Longleftrightarrow K \models \psi(a_1,\dots,a_m), \\ L \models \varphi(a_1,\dots,a_m) &\Longleftrightarrow L \models \psi(a_1,\dots,a_m). \end{align*} Therefore the whole problem has been reduced to the following purely algebraic fact: quantifier-free ordered-ring formulas cannot distinguish $K$ from $L$ when all parameters lie in $K$. [/guided] [/step] [step:Show that all ordered-ring terms evaluate the same way in $K$ and $L$] Let $t(x_1,\dots,x_m)$ be an $\mathcal{L}_{\mathrm{or}}$-term. Denote by \begin{align*} t^K &: K^m \to K, \\ t^L &: L^m \to L \end{align*} the functions induced by interpreting $t$ in $K$ and $L$, respectively. We claim that \begin{align*} t^L(a_1,\dots,a_m) = i\bigl(t^K(a_1,\dots,a_m)\bigr), \end{align*} where $i:K \to L$ is the inclusion map. This is proved by induction on the construction of $t$. For variables and the constants $0,1$, the assertion is immediate from the definition of $i$. If the assertion holds for terms $s$ and $r$, then it holds for $-s$, $s+r$, and $s\cdot r$ because $i$ preserves negation, addition, and multiplication. Hence every ordered-ring term with inputs from $K$ has the same value whether computed in $K$ or in $L$, after applying the inclusion map. [/step] [step:Verify preservation of atomic formulas] Let $s(x_1,\dots,x_m)$ and $t(x_1,\dots,x_m)$ be $\mathcal{L}_{\mathrm{or}}$-terms. By the previous step, \begin{align*} s^L(a) = i(s^K(a)), \qquad t^L(a) = i(t^K(a)). \end{align*} For atomic equalities, since $i:K \to L$ is injective, \begin{align*} K \models s(a)=t(a) &\Longleftrightarrow s^K(a)=t^K(a) \\ &\Longleftrightarrow i(s^K(a))=i(t^K(a)) \\ &\Longleftrightarrow s^L(a)=t^L(a) \\ &\Longleftrightarrow L \models s(a)=t(a). \end{align*} For atomic order relations, because the order on $K$ is the restriction of the order on $L$ along the inclusion, \begin{align*} K \models s(a)<t(a) &\Longleftrightarrow s^K(a)<_K t^K(a) \\ &\Longleftrightarrow i(s^K(a))<_L i(t^K(a)) \\ &\Longleftrightarrow s^L(a)<_L t^L(a) \\ &\Longleftrightarrow L \models s(a)<t(a). \end{align*} Thus $K$ and $L$ agree on every atomic $\mathcal{L}_{\mathrm{or}}$-formula at the tuple $a$. [/step] [step:Pass from atomic formulas to quantifier-free formulas] We prove by induction on the construction of quantifier-free formulas that for every quantifier-free $\mathcal{L}_{\mathrm{or}}$-formula $\theta(x_1,\dots,x_m)$, \begin{align*} K \models \theta(a_1,\dots,a_m) \quad \Longleftrightarrow \quad L \models \theta(a_1,\dots,a_m). \end{align*} The atomic case is exactly the previous step. The Boolean connectives preserve equivalence of truth values: if the equivalence holds for $\theta_1$ and $\theta_2$, then it holds for $\neg \theta_1$, $\theta_1 \wedge \theta_2$, $\theta_1 \vee \theta_2$, and $\theta_1 \to \theta_2$ by the ordinary truth tables for these connectives. Since quantifier-free formulas are built from atomic formulas using only Boolean connectives, the induction proves the claim for $\psi$. [guided] We now extend the atomic agreement to all quantifier-free formulas. A quantifier-free formula is obtained from atomic formulas by applying Boolean connectives finitely many times. There are no quantifiers, so there is no step in which the larger domain $L$ can introduce new witnesses. We argue by structural induction. The base case is an atomic formula, which was proved in the previous step. Suppose the equivalence of truth values between $K$ and $L$ has already been proved for quantifier-free formulas $\theta_1(x_1,\dots,x_m)$ and $\theta_2(x_1,\dots,x_m)$. Then \begin{align*} K \models \neg \theta_1(a) &\Longleftrightarrow \text{not } K \models \theta_1(a) \\ &\Longleftrightarrow \text{not } L \models \theta_1(a) \\ &\Longleftrightarrow L \models \neg \theta_1(a). \end{align*} Likewise, conjunction is preserved because \begin{align*} K \models \theta_1(a)\wedge\theta_2(a) &\Longleftrightarrow \bigl(K \models \theta_1(a) \text{ and } K \models \theta_2(a)\bigr) \\ &\Longleftrightarrow \bigl(L \models \theta_1(a) \text{ and } L \models \theta_2(a)\bigr) \\ &\Longleftrightarrow L \models \theta_1(a)\wedge\theta_2(a). \end{align*} The same truth-table argument applies to disjunction and implication. Therefore every quantifier-free formula has the same truth value in $K$ and in $L$ on tuples from $K$. [/guided] [/step] [step:Conclude that the inclusion is elementary] Applying the previous step to the quantifier-free formula $\psi$ chosen in the first step gives \begin{align*} K \models \psi(a_1,\dots,a_m) \quad \Longleftrightarrow \quad L \models \psi(a_1,\dots,a_m). \end{align*} Combining this equivalence with the $\operatorname{RCF}$-equivalence between $\varphi$ and $\psi$ in both $K$ and $L$, we obtain \begin{align*} K \models \varphi(a_1,\dots,a_m) \quad \Longleftrightarrow \quad L \models \varphi(a_1,\dots,a_m). \end{align*} Since $m$, $\varphi$, and $a \in K^m$ were arbitrary, the inclusion $i:K \to L$ is an elementary embedding. Hence $K \preccurlyeq L$, and $\operatorname{RCF}$ is model complete. [/step]