[proofplan] We prove the contrapositive of the desired avoidance conclusion. If no formula in $p(x)$ can be avoided inside the $T$-consistent definable set $\theta(x)$, then every realization of $\theta(x)$ in every model of $T$ satisfies every formula in $p(x)$. Since $\theta(x)$ is itself consistent with $T$, this means that $\theta(x)$ isolates the type $p(x)$ over $T$, contradicting the assumption that $p(x)$ is non-principal. [/proofplan] [step:Assume every member of $p(x)$ is forced on the $\theta(x)$-locus] Suppose, toward a contradiction, that the conclusion fails. Then for every formula $\varphi(x) \in p(x)$, the theory \begin{align*} T \cup \{\exists x\,(\theta(x) \wedge \neg \varphi(x))\} \end{align*} is not satisfiable. Fix $\varphi(x) \in p(x)$. The unsatisfiability of this theory means that no model $M \models T$ contains a tuple $a \in M^{|x|}$ such that \begin{align*} M \models \theta(a) \wedge \neg \varphi(a). \end{align*} Equivalently, \begin{align*} T \models \forall x\,(\theta(x) \to \varphi(x)). \end{align*} Since $\varphi(x) \in p(x)$ was arbitrary, we have \begin{align*} T \models \forall x\,(\theta(x) \to \varphi(x)) \end{align*} for every $\varphi(x) \in p(x)$. [guided] Assume the desired conclusion is false. This means that every formula belonging to the type $p(x)$ is unavoidable on the definable set cut out by $\theta(x)$: for each $\varphi(x) \in p(x)$, the theory \begin{align*} T \cup \{\exists x\,(\theta(x) \wedge \neg \varphi(x))\} \end{align*} has no model. Fix one formula $\varphi(x) \in p(x)$. What does this unsatisfiability say semantically? It says there is no model $M$ of $T$ and no tuple $a \in M^{|x|}$ such that $a$ realizes $\theta(x)$ but fails $\varphi(x)$. In symbols, there do not exist $M \models T$ and $a \in M^{|x|}$ with \begin{align*} M \models \theta(a) \wedge \neg \varphi(a). \end{align*} That is exactly the same as saying that every tuple satisfying $\theta(x)$ in every model of $T$ also satisfies $\varphi(x)$. Therefore \begin{align*} T \models \forall x\,(\theta(x) \to \varphi(x)). \end{align*} Because the formula $\varphi(x) \in p(x)$ was arbitrary, this implication holds for every member of the type: \begin{align*} T \models \forall x\,(\theta(x) \to \varphi(x)) \end{align*} for all $\varphi(x) \in p(x)$. [/guided] [/step] [step:Use $\theta(x)$ to isolate the type $p(x)$] By hypothesis, \begin{align*} T \cup \{\exists x\,\theta(x)\} \end{align*} is satisfiable. Together with the previous step, this says that $\theta(x)$ is consistent with $T$ and implies every formula in $p(x)$ modulo $T$. Hence $\theta(x)$ isolates $p(x)$ over $T$. Therefore $p(x)$ is principal over $T$, contradicting the assumption that $p(x)$ is non-principal. The contradiction shows that the supposition was false, so there exists $\varphi(x) \in p(x)$ such that \begin{align*} T \cup \{\exists x\,(\theta(x) \wedge \neg \varphi(x))\} \end{align*} is satisfiable. [/step]