[proofplan] The proof uses the isolating formula $\theta(x)$ as a finite witness for the whole type. In an arbitrary model $M \models T$, the sentence $T \models \exists x\,\theta(x)$ guarantees a tuple $a \in M^n$ satisfying $\theta(x)$. Since $\theta(x)$ isolates $p(x)$, every formula belonging to $p(x)$ is forced by $\theta(x)$ over $T$, and therefore holds of the same tuple $a$ in $M$. Thus $a$ realizes all formulas in $p(x)$ simultaneously. [/proofplan] [step:Choose a tuple satisfying the isolating formula in an arbitrary model] Let $M$ be an arbitrary model of $T$. Since $T \models \exists x\,\theta(x)$ and $M \models T$, the sentence $\exists x\,\theta(x)$ holds in $M$. Hence there exists a tuple $a = (a_1,\dots,a_n) \in M^n$ such that \begin{align*} M \models \theta(a). \end{align*} [guided] We begin with an arbitrary model because the theorem claims realization in every model of $T$. Let $M$ be a model satisfying $M \models T$. The hypothesis \begin{align*} T \models \exists x\,\theta(x) \end{align*} means that every model of $T$ satisfies the sentence $\exists x\,\theta(x)$. Since $M$ is one such model, we obtain \begin{align*} M \models \exists x\,\theta(x). \end{align*} By the semantics of the existential quantifier, there is a tuple $a = (a_1,\dots,a_n) \in M^n$ such that \begin{align*} M \models \theta(a). \end{align*} This tuple is the candidate realization of the type $p(x)$. The rest of the proof verifies that it satisfies every formula belonging to $p(x)$, not merely the single formula $\theta(x)$. [/guided] [/step] [step:Use isolation to transfer every formula of the type to the chosen tuple] Let $\varphi(x)$ be an arbitrary formula with $\varphi(x) \in p(x)$. Since $\theta(x)$ isolates $p(x)$, we have \begin{align*} T \models \forall x\,(\theta(x) \to \varphi(x)). \end{align*} Because $M \models T$, it follows that \begin{align*} M \models \forall x\,(\theta(x) \to \varphi(x)). \end{align*} Evaluating this universal sentence at the tuple $a \in M^n$ gives \begin{align*} M \models \theta(a) \to \varphi(a). \end{align*} Together with $M \models \theta(a)$, this yields \begin{align*} M \models \varphi(a). \end{align*} [/step] [step:Conclude that the chosen tuple realizes the type] The formula $\varphi(x) \in p(x)$ was arbitrary, so the same tuple $a \in M^n$ satisfies \begin{align*} M \models \varphi(a) \end{align*} for every $\varphi(x) \in p(x)$. Therefore $a$ realizes $p(x)$ in $M$. Since $M \models T$ was arbitrary, every model of $T$ realizes $p(x)$. [/step]