Proof of the General Principle of Induction

Assume the antecedent of the principle, eliminating the defined notation for $\mathit{HerOn}(F,{}^{a}R^{+})$:

$Pa\amp \forall x,y(R^{+}(a,x)\amp R^{+}(a,y)\amp Rxy\rightarrow (Px\rightarrow Py))$

We want to show, for an arbitrary object $b$, that if $R ^{+}(a,b)$ then $Pb$. So assume $R^{+}(a,b)$. To show $Pb$, we appeal to Fact (7) about $R^{+}$ (in our subsection on the Weak Ancestral in §4):

$Fx\amp R^{+}(x,y)\amp \mathit{Her}(F,R)\rightarrow Fy$

Instantiate the variable $F$ in this Fact to the property $[\lambda z \, R^{+}(a,z)\amp Pz]$ (that there is such a property is guaranteed by the Comprehension Principle for Relations), and instantiate the variables $x$ and $y$ to the objects $a$ and $b$, respectively. The result (after applying $\lambda$-Conversion) is therefore something that we have established as true:

$R^{+}(a,a)\amp Pa\amp R^{+}(a,b)\amp \mathit{Her}([\lambda z \, R^{+}(a,z)\amp Pz], R)\rightarrow$
    $R^{+}(a,b)\amp Pb$

So if we can establish the antecedent of this fact, we establish $Pb$. But we know that the first conjunct is true, by the definition of $R^{+}$. We know the second conjunct is true, by assumption. We know that the third conjunct is true, by further assumption. So if we can establish:

$\mathit{Her}([\lambda z \, R^{+}(a,z)\amp Pz], R)$,

we are done. But, by the definition of heredity, this just means:

$\forall x,y[Rxy\rightarrow ((R^{+}(a,x)\amp Px) \rightarrow (R^{+}(a,y)\amp Py))]$.

To prove this claim, we assume $Rxy$ and $R^{+}(a,x)\amp Px$ (to show $R^{+}(a,y)\amp Py$). But from the facts that $R^{+}(a,x)$ and $Rxy$, it follows from Fact (3) about $R^{+}$ (in our subsection on the Weak Ancestral) that $R^{*}(a,y)$. This implies $R^{+}(a,y)$, by the definition of $R^{+}$. But since we now have $R^{+}(a,x), R^{+}(a,y), Rxy$, and $Px$, it follows from the first assumption in the proof that $Py$.