Zunächst ist ${\displaystyle {}\Gamma =I^{\vDash }}$ aufgrund des Korrektheitssatzes abgeschlossen unter Ableitungen. Für jeden ${\displaystyle {}S}$-Ausdruck ${\displaystyle {}\alpha }$ gilt die Alternative: Entweder ${\displaystyle {}\alpha \in \Gamma }$ oder ${\displaystyle {}\neg \alpha \in \Gamma }$. Insbesondere ist ${\displaystyle {}\Gamma }$ widerspruchsfrei. Wenn ${\displaystyle {}\alpha \not \in \Gamma }$ ist, so ist ${\displaystyle {}\neg \alpha \in \Gamma }$ und daher ist ${\displaystyle {}\Gamma \cup \{\alpha \}}$ widersprüchlich. Also ist ${\displaystyle {}\Gamma }$ maximal widerspruchsfrei.
Wir betrachten nun einen Ausdruck der Form ${\displaystyle {}\alpha =\exists x\beta }$. Wenn ${\displaystyle {}\alpha \notin \Gamma }$ gilt, so gilt ${\displaystyle {}\exists x\beta \rightarrow \beta {\frac {t}{x}}}$ in ${\displaystyle {}I}$ für jeden Term ${\displaystyle {}t}$, da ja der Vordersatz nicht gilt. Wenn hingegen ${\displaystyle {}\alpha \in \Gamma }$ gilt, so gibt es aufgrund des semantischen Aufbaus der Gültigkeitbeziehung ein ${\displaystyle {}m\in M}$ derart, dass ${\displaystyle {}I{\frac {m}{x}}\vDash \beta }$ gilt. Wegen der vorausgesetzten Surjektivität der Belegung gibt es einen Term ${\displaystyle {}t}$, der durch ${\displaystyle {}m}$ interpretiert wird. Daher gilt nach dem Substitutionslemma ${\displaystyle {}\beta {\frac {t}{x}}}$ in ${\displaystyle {}I}$. Also gilt ${\displaystyle {}\exists x\beta \rightarrow \beta {\frac {t}{x}}}$ in ${\displaystyle {}I}$.