Es sei ${\displaystyle {}\Gamma }$ eine widerspruchsfreie Menge an ${\displaystyle {}S}$-Ausdrücken (über einem Symbolalphabet ${\displaystyle {}S}$).

Dann gibt es eine Symbolerweiterung ${\displaystyle {}S^{*}\supseteq S}$ und eine widerspruchsfreie ${\displaystyle {}S^{*}}$-Ausdrucksmenge ${\displaystyle {}\Gamma ^{*}\supseteq \Gamma }$ derart, dass es zu jedem Ausdruck ${\displaystyle {}\exists x\alpha \in L^{S}}$ einen Term ${\displaystyle {}t}$ (über ${\displaystyle {}S^{*}}$) derart gibt, dass

gilt.