Stable trace of a definable set (source code)

= Stable trace of a definable set

If $T$ is stable, $M\preccurlyeq N\models T$, and $X\subseteq N^n$ is definable with parameters from $N$, then $X\cap M^n$ is definable with parameters from $M$. Apply definability of the type over $M$ of the parameter defining $X$.