Es sei ein Symbolalphabet S {\displaystyle {}S} einer Sprache erster Stufe gegeben. Es seien x 1 , … , x k , y 1 , … , y ℓ {\displaystyle {}x_{1},\ldots ,x_{k},y_{1},\ldots ,y_{\ell }} paarweise verschiedene Variablen und t 1 , … , t k , s 1 , … , s ℓ {\displaystyle {}t_{1},\ldots ,t_{k},s_{1},\ldots ,s_{\ell }} fixierte S {\displaystyle {}S} -Terme. Zeige, dass für Terme τ {\displaystyle {}\tau } , in denen y 1 , … , y ℓ {\displaystyle {}y_{1},\ldots ,y_{\ell }} nicht vorkommen, die Gleichheit
einer
Sprache erster Stufe
gegeben. Es seien 
paarweise verschiedene Variablen und 
fixierte
-Terme.
Zeige, dass für Terme 
, in denen 
nicht vorkommen, die Gleichheit
