Prädikatenlogik/Alleinführung im Sukzedens/Regel/Axiom

Es sei ein Symbolalphabet erster Stufe, und seien -Ausdrücke, und seien Variablen. Dann gilt unter der Bedingung, dass weder in noch in frei vorkommt die folgende Regel: Aus

folgt