証明の都合上、(GEN')のステートメントの\(\xi\)と\(\zeta\)を入れ替えておき、\(\varphi\)は\(\psi\)に直す。また両命題の固有変数条件の表記を揃えた。
(GEN)\(\fbox{$\varphi[\zeta/\xi]\Rightarrow\forall\xi\varphi$}\)、ただし\(\varphi[\zeta/\xi]\)の演繹の前提に含まれる論理式を\(\Gamma\)とするとき、\(\zeta\notin{\rm fv}(\Gamma)\)。\(\zeta\notin{\rm fv}(\varphi)-\{\xi\}\)。
(GEN')\(\fbox{$\psi\Rightarrow\forall\xi(\psi[\xi/\zeta])$}\)、ただし\(\psi\)の演繹の前提に含まれる論理式を\(\Gamma\)とするとき、\(\zeta\notin{\rm fv}(\Gamma)\)。\(\xi\notin{\rm fv}(\psi)-\{\zeta\}\)。
自由変数に関する補題を見ておく。\(\theta,\eta\)を変項（\(\theta\equiv\eta\)でもよい）、\(\chi\)を論理式とする。
【補題1】\(\theta\notin{\rm fv}(\chi[\eta/\theta])-\{\eta\}\)。
（証明）\(\theta\not\equiv\eta\)と仮定すると、\(\theta\in{\rm fv}(\chi)\)か否かにかかわらず\(\theta\not\in{\rm fv}(\chi[\eta/\theta])\)である。
【補題2】\(\eta\notin{\rm fv}(\chi)-\{\theta\}\)のとき\(\chi[\eta/\theta][\theta/\eta]\equiv\chi\)。
（証明）定理5.42(1)(3)による。
(GEN)の\(\varphi\)として\(\psi[\xi/\zeta]\)を、また(GEN')の\(\psi\)として\(\varphi[\zeta/\xi]\)を選べば、補題1により固有変数条件は満たされ、補題2によりもう一方の推論図式が得られる。■
