Omitting types theorem

Let $T$ be a consistent theory in a countable first-order language. For every countable family of nonisolated finite-arity types of $T$, there is a countable model of $T$ that omits every type in the family.

Let $p(\mathbf{x})$ be a nonprincipal partial type over a consistent first-order theory $T$. Suppose $T\cup \{\sigma (\mathbf{c})\}$ is consistent, with $\sigma$ a finite condition in finitely many new constants, and let $\mathbf{t}(\mathbf{c})$ be a tuple of closed terms. Some $\psi \in p$ leaves $T\cup \{\sigma (\mathbf{c}),\neg \psi (\mathbf{t}(\mathbf{c}))\}$ consistent. Otherwise the original-language first-order formulais consistent with $T$ and entails every member of $p$, contradicting nonprincipality. Replace all new constants occurring in the condition or terms by variables. This lemma makes the omission requirements dense in a countable Henkin construction.