Frayne embedding lemma (source code)

= Frayne embedding lemma
{c}

If $A\equiv B$, the elementary diagram of $B$ is finitely satisfiable by interpreting its finitely many named elements in $A$. Choose those finite realizations as coordinates, extend the filter of diagram cones to an <ultrafilter>, and use the <Łoś theorem> to embed $B$ elementarily into an <ultrapower> of $A$. If $A\prec B$, work over the named elements of $A$ and keep their coordinates constant. The resulting embedding extends the diagonal map of $A$. This relative assertion allows an alternating chain of ultrapowers to keep every previously embedded substructure fixed.