Finitely satisfiable type is realized in an elementary extension (source code)

= Finitely satisfiable type is realized in an elementary extension

If a type $p(x)$ over a structure $M$ is finitely satisfiable in $M$, then the elementary diagram of $M$ together with $p(c)$ is finitely satisfiable. Compactness gives an elementary extension of $M$ realizing $p$.