[proofplan] We use quantifier elimination for real closed fields. Given an arbitrary ordered-ring formula, quantifier elimination replaces it modulo $\operatorname{RCF}$ by a quantifier-free formula built from polynomial equalities and order inequalities. An ordered-field embedding preserves the values of all ordered-ring terms and therefore preserves and reflects every atomic polynomial equality and inequality. A structural induction on quantifier-free formulas then gives preservation and reflection for the quantifier-free replacement, hence for the original formula. [/proofplan]

[step:Replace the given formula by an equivalent quantifier-free formula]Let $\varphi(x_1,\dots,x_n)$ be an $\mathcal{L}_{\mathrm{or}}$-formula. By quantifier elimination for real closed 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_n)$ such that \begin{align*} \operatorname{RCF} \models \forall x_1 \cdots \forall x_n\, \bigl(\varphi(x_1,\dots,x_n) \leftrightarrow \psi(x_1,\dots,x_n)\bigr). \end{align*} Since both $K$ and $L$ are real closed fields, they are models of $\operatorname{RCF}$. Therefore, for every $a = (a_1,\dots,a_n) \in K^n$, \begin{align*} K \models \varphi(a_1,\dots,a_n) &\Longleftrightarrow K \models \psi(a_1,\dots,a_n), \\ L \models \varphi(\iota(a_1),\dots,\iota(a_n)) &\Longleftrightarrow L \models \psi(\iota(a_1),\dots,\iota(a_n)). \end{align*}[/step]

[guided]The point of model completeness is to prove preservation of all first-order formulas under embeddings. Quantifier elimination gives a stronger normal form: every formula is equivalent, over real closed fields, to one with no quantifiers. We apply that theorem to the specific formula $\varphi(x_1,\dots,x_n)$. Thus there is a quantifier-free formula $\psi(x_1,\dots,x_n)$ satisfying \begin{align*} \operatorname{RCF} \models \forall x_1 \cdots \forall x_n\, \bigl(\varphi(x_1,\dots,x_n) \leftrightarrow \psi(x_1,\dots,x_n)\bigr). \end{align*} The hypothesis needed here is exactly that we are working in the theory $\operatorname{RCF}$ in the ordered-ring language. Since $K$ and $L$ are real closed fields, each is a model of $\operatorname{RCF}$, so the displayed equivalence holds inside both structures. Hence, for each tuple $a = (a_1,\dots,a_n) \in K^n$, \begin{align*} K \models \varphi(a_1,\dots,a_n) &\Longleftrightarrow K \models \psi(a_1,\dots,a_n), \\ L \models \varphi(\iota(a_1),\dots,\iota(a_n)) &\Longleftrightarrow L \models \psi(\iota(a_1),\dots,\iota(a_n)). \end{align*} It remains only to prove that the embedding $\iota$ preserves and reflects the quantifier-free formula $\psi$.[/guided]

[step:Show that the embedding preserves and reflects atomic ordered-ring formulas]Let $t(x_1,\dots,x_n)$ be an $\mathcal{L}_{\mathrm{or}}$-term. We claim that for every $a = (a_1,\dots,a_n) \in K^n$, \begin{align*} \iota\bigl(t^K(a_1,\dots,a_n)\bigr) = t^L(\iota(a_1),\dots,\iota(a_n)), \end{align*} where $t^K$ and $t^L$ denote the interpretations of $t$ in $K$ and $L$, respectively. This follows by induction on the construction of $t$, using that $\iota$ preserves $0$, $1$, addition, negation, subtraction, and multiplication. Now let $\alpha(x_1,\dots,x_n)$ be an atomic $\mathcal{L}_{\mathrm{or}}$-formula. Atomic formulas are of the forms $s=t$ and $s<t$, where $s$ and $t$ are $\mathcal{L}_{\mathrm{or}}$-terms. If $\alpha$ is $s=t$, then \begin{align*} K \models s(a)=t(a) &\Longleftrightarrow s^K(a)=t^K(a) \\ &\Longleftrightarrow \iota(s^K(a))=\iota(t^K(a)) \\ &\Longleftrightarrow s^L(\iota(a))=t^L(\iota(a)) \\ &\Longleftrightarrow L \models s(\iota(a))=t(\iota(a)), \end{align*} where injectivity of $\iota$ gives the reflection of equality. If $\alpha$ is $s<t$, then because $\iota$ is an embedding of ordered fields, it preserves and reflects the order relation, so \begin{align*} K \models s(a)<t(a) &\Longleftrightarrow s^K(a)<t^K(a) \\ &\Longleftrightarrow \iota(s^K(a))<\iota(t^K(a)) \\ &\Longleftrightarrow s^L(\iota(a))<t^L(\iota(a)) \\ &\Longleftrightarrow L \models s(\iota(a))<t(\iota(a)). \end{align*} Thus every atomic ordered-ring formula is preserved and reflected by $\iota$.[/step]

[guided]A quantifier-free formula is built from atomic formulas using Boolean connectives, so we first handle the atomic formulas. The terms in the ordered-ring language are exactly expressions built from variables, $0$, $1$, addition, negation, subtraction, and multiplication. Since $\iota:K \to L$ is an $\mathcal{L}_{\mathrm{or}}$-embedding, it preserves each of these symbols. Formally, for every $\mathcal{L}_{\mathrm{or}}$-term $t(x_1,\dots,x_n)$ and every tuple $a=(a_1,\dots,a_n)\in K^n$, induction on the construction of $t$ gives \begin{align*} \iota\bigl(t^K(a_1,\dots,a_n)\bigr) = t^L(\iota(a_1),\dots,\iota(a_n)). \end{align*} The base cases are variables and the constants $0,1$. The inductive steps are addition, negation, subtraction, and multiplication, each using the corresponding preservation property of the field embedding. Now consider an atomic formula. Such a formula is either $s=t$ or $s<t$ for ordered-ring terms $s$ and $t$. For equality, injectivity of $\iota$ is what gives reflection: \begin{align*} K \models s(a)=t(a) &\Longleftrightarrow s^K(a)=t^K(a) \\ &\Longleftrightarrow \iota(s^K(a))=\iota(t^K(a)) \\ &\Longleftrightarrow s^L(\iota(a))=t^L(\iota(a)) \\ &\Longleftrightarrow L \models s(\iota(a))=t(\iota(a)). \end{align*} For order, the embedding is an ordered-field embedding, so it preserves and reflects $<$: \begin{align*} K \models s(a)<t(a) &\Longleftrightarrow s^K(a)<t^K(a) \\ &\Longleftrightarrow \iota(s^K(a))<\iota(t^K(a)) \\ &\Longleftrightarrow s^L(\iota(a))<t^L(\iota(a)) \\ &\Longleftrightarrow L \models s(\iota(a))<t(\iota(a)). \end{align*} Thus every atomic condition appearing in a quantifier-free ordered-ring formula has the same truth value in $K$ at $a$ and in $L$ at $\iota(a)$.[/guided]

[step:Extend preservation from atomic formulas to quantifier-free formulas] We prove by induction on the construction of the quantifier-free formula $\psi$ that, for every $a \in K^n$, \begin{align*} K \models \psi(a) \quad \Longleftrightarrow \quad L \models \psi(\iota(a)). \end{align*} The atomic case was proved in the previous step. The Boolean connectives are immediate from the induction hypothesis: negation reverses truth values on both sides, conjunction requires both conjuncts on both sides, and disjunction requires at least one disjunct on both sides. Therefore the equivalence holds for the quantifier-free formula $\psi$ obtained from quantifier elimination. [/step]

[step:Transfer the original formula and conclude elementarity] Combining the equivalence between $\varphi$ and $\psi$ in both real closed fields with the preservation and reflection of $\psi$ gives \begin{align*} K \models \varphi(a) &\Longleftrightarrow K \models \psi(a) \\ &\Longleftrightarrow L \models \psi(\iota(a)) \\ &\Longleftrightarrow L \models \varphi(\iota(a)). \end{align*} This holds for every $\mathcal{L}_{\mathrm{or}}$-formula $\varphi(x_1,\dots,x_n)$ and every tuple $a \in K^n$. Hence $\iota:K \to L$ is an elementary embedding. Since $K$, $L$, and $\iota$ were arbitrary, every embedding between models of $\operatorname{RCF}$ is elementary, so $\operatorname{RCF}$ is model complete. [/step]