Solution (source code)

= Solution

Name every element $a\in A$ by a new constant $c_a$, distinct from the symbols already in $L'$. Let $\operatorname{Diag}(A)$ be its full atomic and negated atomic <diagram of a structure>. A model of this diagram contains an isomorphic copy of $A$ as an $L$-<substructure>. We claim
$$
T'\cup\operatorname{Diag}(A)
$$
is satisfiable.

Otherwise <compactness theorem> gives a finite diagram conjunction $\delta(c_{a_1},\ldots,c_{a_m})$ inconsistent with $T'$. Replace these new constants by variables. Since $T'$ says nothing about the new names, it then entails the <universal sentence>
$$
\forall x_1\cdots\forall x_m\,\neg\delta(x_1,\ldots,x_m).
$$
The conjunction $\delta$ uses only symbols of $L$, so this is one of the universal $L$-consequences assumed true in $A$. But $A$ satisfies $\delta(a_1,\ldots,a_m)$, a contradiction. A model of the consistent enlarged theory gives \b[an embedding of $A$ into the $L$-reduct of a model of $T'$]. Negated atomic facts and disequalities in the diagram ensure that this is a <structure embedding>, not merely a homomorphism.