Proof of the General Principle of Induction

Assume the antecedent of the principle, eliminating the defined notation for HerOn(F, ^aR⁺):

Pa & ∀x,y(R⁺(a,x) & R⁺(a,y) & Rxy → (Px → 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 & R⁺(x,y) & Her(F,R) → Fy

Instantiate the variable F in this Fact to the property [λz R⁺(a,z) & 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 λ-Conversion) is therefore something that we have established as true:

R⁺(a,a) & Pa & R⁺(a,b) & Her([λz R⁺(a,z) & Pz], R) →
    R⁺(a,b) & 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:

Her([λz R⁺(a,z) & Pz], R),

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

∀x,y[Rxy → ((R⁺(a,x) & Px) → (R⁺(a,y) & Py))].

To prove this claim, we assume Rxy and R⁺(a,x) & Px (to show: R⁺(a,y) & 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.