Das Symbolalphabet bestehe neben Variablen aus einer Konstanten und einem zweistelligen Funktionssymbol . Es sei
die Menge aller Ableitungen aus dem Axiomensystem
-
Es sei die zugehörige Äquivalenzrelation gemäß
Bemerkung.
Zeige
für jedes Variablenpaar .