[proofplan] We prove the contrapositive. Assume that some complete type over the empty set is realized but not isolated. The restricted omitting hypothesis gives a countable model omitting that type, while compactness and downward Löwenheim-Skolem give a countable model realizing it. Since realization of a type over the empty set is preserved under isomorphism, these two countable models cannot be isomorphic. [/proofplan] [step:Choose a realized non-isolated type and obtain a countable model omitting it] Assume, toward the contrapositive, that there exist an integer $n \geq 1$ and a complete type $p(x_1,\dots,x_n) \in S_n(T)$ such that $p$ is realized in some model of $T$ and $p$ is not isolated. By the hypothesis applied to this non-isolated type, there exists a countable model $M \models T$ such that no tuple $a \in M^n$ realizes $p$. We say that $M$ omits $p$. [/step] [step:Construct a countable model realizing the same type] Since $p$ is realized in some model of $T$, choose a model $N_0 \models T$ and a tuple $b \in N_0^n$ such that $N_0 \models \varphi(b)$ for every formula $\varphi(x_1,\dots,x_n) \in p$. By the [downward Löwenheim-Skolem theorem](/theorems/4299) with parameters, applied to the countable language $L$, the structure $N_0$, and the finite parameter set $\{b_1,\dots,b_n\}$, there exists a countable elementary substructure $N \preccurlyeq N_0$ such that $b \in N^n$. Because $N \preccurlyeq N_0$ and $N_0 \models T$, we have $N \models T$. Moreover, for each formula $\varphi(x_1,\dots,x_n) \in p$, elementarity gives \begin{align*} N \models \varphi(b) \end{align*} because \begin{align*} N_0 \models \varphi(b). \end{align*} Thus the countable model $N \models T$ realizes $p$. [guided] We need a countable model realizing the same type $p$, not merely some large model realizing it. By assumption, $p$ is realized in some model of $T$, so there are a model $N_0 \models T$ and a tuple $b = (b_1,\dots,b_n) \in N_0^n$ such that every formula in $p$ holds of $b$ in $N_0$. The obstacle is that $N_0$ may be uncountable. We use the [downward Löwenheim-Skolem theorem](/theorems/4272) with parameters: because the language $L$ is countable and the parameter set $\{b_1,\dots,b_n\}$ is finite, there is a countable elementary substructure $N \preccurlyeq N_0$ containing each coordinate of $b$. The containment condition is important: it ensures that $b$ is still a tuple from the smaller model, so it makes sense to ask whether $N$ realizes $p$ by $b$. Since $N \preccurlyeq N_0$, every first-order formula with parameters from $N$ has the same truth value in $N$ and in $N_0$. In particular, for each formula $\varphi(x_1,\dots,x_n) \in p$, the tuple $b \in N^n$ satisfies \begin{align*} N_0 \models \varphi(b). \end{align*} Elementarity therefore gives \begin{align*} N \models \varphi(b). \end{align*} Hence $b$ realizes every formula in $p$ inside $N$. Also, since $N$ is an elementary substructure of a model of $T$, it satisfies every sentence of $T$. Therefore $N$ is a countable model of $T$ realizing $p$. [/guided] [/step] [step:Use isomorphism invariance of types to separate the two countable models] We claim that $M$ and $N$ are not isomorphic. Suppose instead that there were an isomorphism \begin{align*} f: M &\to N. \end{align*} Let $b \in N^n$ be the tuple realizing $p$ in $N$, and define $a \in M^n$ by \begin{align*} a_i := f^{-1}(b_i) \end{align*} for each $i \in \{1,\dots,n\}$. For every formula $\varphi(x_1,\dots,x_n) \in p$, satisfaction is preserved by isomorphism, so \begin{align*} M \models \varphi(a) \end{align*} because \begin{align*} N \models \varphi(f(a)) = \varphi(b). \end{align*} Thus $a$ realizes $p$ in $M$, contradicting the construction of $M$ as a model omitting $p$. Therefore $M$ and $N$ are non-isomorphic countable models of $T$. [/step] [step:Conclude the contrapositive] We have shown that if some complete type over the empty set is realized in a model of $T$ but is not isolated, then $T$ has two non-isomorphic countable models. This is the contrapositive of the desired implication. Hence, if $T$ has exactly one countable model up to isomorphism, every complete type over the empty set realized in some model of $T$ is isolated. [/step]