Realization of a type in an elementary extension (source code)

= Realization of a type in an elementary extension

Every complete type over parameters from $M$ is realized in some elementary extension of $M$. Apply compactness to the elementary diagram of $M$ together with a new tuple of constants satisfying the type.