diff --git a/iii/mtncl/02_quantifier_elimination.tex b/iii/mtncl/02_quantifier_elimination.tex
index 9f69415..7966489 100644
--- a/iii/mtncl/02_quantifier_elimination.tex
+++ b/iii/mtncl/02_quantifier_elimination.tex
@@ -381,11 +381,11 @@ \subsection{Characterisations of quantifier elimination}
     as required.
 
     \emph{(iii) implies (iv).}
-    It suffices to show that any universal formula \( \varphi(\vb x) \) is preserved under embeddings.
-    If so, then \( \varphi(\vb x) \) is equivalent to an existential \( \mathcal L \)-formula, so in particular, any existential formula is equivalent to a universal formula.
-    Let \( e : \mathcal A \rightarrowtail \mathcal B \) be an embedding.
-    Then by (iii) we have an elementary extension \( \mathcal A \preceq \mathcal D \), so if \( \mathcal A \vDash \varphi(\vb a) \), then \( \mathcal D \vDash \varphi(\vb a) \), and as \( \mathcal B \) is a substructure of \( \mathcal D \), we have \( \mathcal B \vDash \varphi(e(\vb a)) \).
-    The reverse implication follows from the fact that \( \varphi \) is universal.
+    By the theorem of Tarski and \L{}o\'s characterising theories preserved under substructures, it suffices to show that existential formulas are preserved under substructures.
+    Let \( e : \mathcal A \to \mathcal B \) be such that \( \mathcal B \vDash \varphi(e(\vb a)) \), where \( \varphi \) is an existential formula, and \( \vb a \in \mathcal A \).
+    By (ii), there is an elementary extension \( \mathcal D \) of \( \mathcal A \) and an embedding \( g : \mathcal B \rightarrowtail \mathcal D \) such that \( g \circ e = \id_{\mathcal A} \).
+    Existential formulas are preserved under extensions, so \( \mathcal D \vDash \varphi(\vb a) \).
+    As \( \mathcal A \preceq \mathcal D \), we must have \( \mathcal A \vDash \varphi(\vb a) \), as required.
 
     \emph{(iv) implies (v).}
     We proceed by induction on the structure of \( \mathcal L \)-formulae.
@@ -500,7 +500,7 @@ \subsection{Characterisations of quantifier elimination}
 \begin{corollary}
     Let \( \mathcal T \) be an \( \mathcal L \)-theory such that
     \begin{enumerate}
-        \item If \( \mathcal A, \mathcal B \vDash \mathcal T \) with \( \mathcal A \subseteq \mathcal B \), and \( \varphi(\vb x, y) \) is a quantifier-free formula, then for all \( \vb a \in \mathcal A \),
+        \item \( \mathcal T \) preserves existential formulas under substructures: if \( \mathcal A, \mathcal B \vDash \mathcal T \) with \( \mathcal A \subseteq \mathcal B \), and \( \varphi(\vb x, y) \) is a quantifier-free formula, then for all \( \vb a \in \mathcal A \),
         \[ (\mathcal B \vDash \exists y.\, \varphi(\vb a, y)) \implies (\mathcal A \vDash \exists y.\, \varphi(\vb a, y)) \]
         \item For any \( \mathcal C \subseteq \mathcal A \vDash \mathcal T \), there is an \emph{initial intermediate model} \( \mathcal A' \vDash \mathcal T \): that is, \( \mathcal C \subseteq \mathcal A' \subseteq \mathcal A \), and for any other model \( \mathcal C \subseteq \mathcal B \subseteq \mathcal A \), there is an embedding \( \mathcal A' \rightarrowtail \mathcal B \) that fixes \( \mathcal C \).
     \end{enumerate}
@@ -517,16 +517,27 @@ \subsection{Characterisations of quantifier elimination}
     If we can do this, we can iterate the process to obtain a chain of elementary extensions
     \[ \mathcal B \preceq \mathcal B_0 \preceq \mathcal B_1 \preceq \dots \preceq \mathcal B_{k-1} \]
     and elements \( d_i \in \mathcal B_i \) such that \( (\mathcal A, \vb a, \vb c) \equiv_0 (\mathcal B, \vb b, \vb d) \).
-    Then \( \mathcal B_{k-1} \vDash \varphi(\vb b, \vb d) \) as \( \varphi \) is quantifier-free, so \( \mathcal B_{k-1} \vDash \exists y.\, \varphi(\vb b, \vb y) \), giving \( \mathcal B \vDash \exists y.\, \varphi(\vb b, \vb y) \) as \( \mathcal B_{k-1} \equiv \mathcal B \) as required.
+    Then \( \mathcal B_{k-1} \vDash \varphi(\vb b, \vb d) \) as \( \varphi \) is quantifier-free, so \( \mathcal B_{k-1} \vDash \exists \vb y.\, \varphi(\vb b, \vb y) \), giving \( \mathcal B \vDash \exists \vb y.\, \varphi(\vb b, \vb y) \) as \( \mathcal B_{k-1} \equiv \mathcal B \) as required.
 
     To find \( \mathcal B_0 \) and \( d_0 \), we use the hypotheses and the compactness theorem.
-    As \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \), there is an isomorphism \( \langle \vb a \rangle_{\mathcal A} \to \langle \vb b \rangle_{\mathcal B} \).
+    As \( (\mathcal A, \vb a) \equiv_0 (\mathcal B, \vb b) \), there is an isomorphism \( \langle \vb a \rangle_{\mathcal A} \to \langle \vb b \rangle_{\mathcal B} \) mapping \( \vb a \) to \( \vb b \).
     Take \( \mathcal C = \langle \vb a \rangle_{\mathcal A} \subseteq \mathcal A \).
     By hypothesis (ii), there is an initial intermediate model \( \mathcal C \subseteq \mathcal A' \subseteq \mathcal A \) with \( \mathcal A' \vDash \mathcal T \), and there is an embedding \( \mathcal A' \rightarrowtail \mathcal B \) fixing \( \mathcal C \).
     Without loss of generality, let us assume that this embedding is an inclusion.
+    % https://q.uiver.app/#q=WzAsNSxbMCwyLCJcXGxhbmdsZSBcXHZiIGEgXFxyYW5nbGVfe1xcbWF0aGNhbCBBfSJdLFsxLDIsIlxcbGFuZ2xlIFxcdmIgYiBcXHJhbmdsZV97XFxtYXRoY2FsIEJ9Il0sWzAsMSwiXFxtYXRoY2FsIEEnIl0sWzEsMCwiXFxtYXRoY2FsIEIiXSxbMCwwLCJcXG1hdGhjYWwgQSJdLFswLDEsIlxcc2ltIl0sWzAsMl0sWzEsM10sWzIsNF0sWzIsMywiIiwyLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibW9ubyJ9fX1dXQ==
+\[\begin{tikzcd}
+	{\mathcal A} & {\mathcal B} \\
+	{\mathcal A'} \\
+	{\langle \vb a \rangle_{\mathcal A}} & {\langle \vb b \rangle_{\mathcal B}}
+	\arrow[from=2-1, to=1-1]
+	\arrow[tail, from=2-1, to=1-2]
+	\arrow[from=3-1, to=2-1]
+	\arrow["\sim", from=3-1, to=3-2]
+	\arrow[from=3-2, to=1-2]
+\end{tikzcd}\]
     Write
     \[ \Psi = \qty{\psi(\vb x, y) \mid \mathcal A \vDash \psi(\vb a, c_0),\, \psi \text{ quantifier-free}} \]
-    As \( \vb a \in \mathcal A' \), we have that \( \mathcal A' \vDash \exists y.\, \psi(\vb a, y) \) for all \( \psi \in \Psi \) by hypothesis (a).
+    As \( \vb a \in \mathcal A' \), we have that \( \mathcal A' \vDash \exists y.\, \psi(\vb a, y) \) for all \( \psi \in \Psi \) by hypothesis (i).
     Now, \( \mathcal A' \subseteq \mathcal B \), and existential formulae are preserved under extension, so \( \mathcal B \vDash \exists y.\, \psi(\vb b, y) \) for all \( \psi \in \Psi \).
     We conclude that every finite subset of \( \Psi \) is satisfied by some element of \( \mathcal B \), as finite conjunctions of quantifier-free formulae are also quantifier-free.
     Thus, by compactness, there is an elementary extension \( \mathcal B \preceq \mathcal B_0 \) and \( d_0 \in \mathcal B_0 \) satisfying the formulae in \( \Psi \).
@@ -541,7 +552,7 @@ \subsection{Applications}
     We will assume that every ordered field has a \emph{real closure}, and that a real closed field satisfies the intermediate value theorem for polynomials.
 
     We show that hypothesis (i) of the corollary above holds.
-    Suppose we have an embedding \( \mathcal A \subseteq \mathcal B \) of real closed fields, \( \vb a \in A \), and a quantifier-free formula \( \varphi(\vb x, y) \) such that \( \mathcal B \vDash \exists y.\, \varphi(\vb a, y) \).
+    Suppose we have an embedding \( \mathcal A \subseteq \mathcal B \) of real closed fields, \( \vb a \in \mathcal A \), and a quantifier-free formula \( \varphi(\vb x, y) \) such that \( \mathcal B \vDash \exists y.\, \varphi(\vb a, y) \).
     By considering the disjunctive normal form, we may assume that \( \varphi \) is a disjunction of a conjunction of literals.
     Moreover, the formulae \( y \neq z \) and \( y \nless z \) can be written in terms of \( = \) and \( < \).
     Thus, we may assume that \( \varphi(\vb a, y) \) is of the form
@@ -567,12 +578,12 @@ \subsection{Applications}
     The embedding \( \mathcal C \) into \( \mathcal A \) is an injective homomorphism of ordered rings, into an ordered field.
     By the universal property of the fraction field, there is a unique homomorphism of ordered fields from \( FF(\mathcal C) \) to \( \mathcal A \) that extends the inclusion of \( \mathcal C \) into \( \mathcal A \).
     Let \( \mathcal A' \) be the real closure of \( FF(\mathcal C) \), so that \( \mathcal C \subseteq FF(\mathcal C) \subseteq \mathcal A' \subseteq \mathcal A \).
-    If \( \mathcal B \vDash \mathsf{RCF} \) and \( \mathcal C \subseteq B \), then by the same argument we have a unique ordered ring homomorphism \( FF(\mathcal C) \to \mathcal B \) extending the embedding \( \mathcal C \subseteq \mathcal B \).
+    If \( \mathcal B \vDash \mathsf{RCF} \) and \( \mathcal C \subseteq \mathcal B \), then by the same argument we have a unique ordered ring homomorphism \( FF(\mathcal C) \to \mathcal B \) extending the embedding \( \mathcal C \subseteq \mathcal B \).
     Thus \( \mathcal A' \subseteq \mathcal B \) as well, and this embedding fixes \( \mathcal C \).
 \end{example}
 \begin{corollary}[Hilbert's Nullstellensatz]
     Let \( k \) be an algebraically closed field, and \( I \) be a proper ideal of \( k[x_1, \dots, x_n] \).
-    Then there exists \( \vb a \in k^n \) such that \( f(\vb a) = 0 \) for all \( I \in f \).
+    Then there exists \( \vb a \in k^n \) such that \( f(\vb a) = 0 \) for all \( f \in I \).
 \end{corollary}
 \begin{proof}
     By Zorn's lemma, every proper ideal can be extended to a maximal ideal, so without loss of generality we may assume that \( I \) is a maximal ideal.