 When we expand the defined notation for \(\mathit{HerOn}\), substitute the notation \(Nx\) and \(Ny\) for \(\mathit{Precedes}^{+}(0,x)\) and \(\mathit{Precedes}^{+}(0,y)\), respectively, and then employ our restricted quantifiers \(\forall n(\ldots n\ldots)\) and \(\forall m(\ldots m\ldots)\) for the claims of the form \(\forall y(Ny \to \ldots y\ldots)\) and \(\forall x(Nx \to \ldots x\ldots)\), respectively, the result is the Principle of Mathematical Induction (in which the notation \(\mathit{HerOn}(F,N)\) has been eliminated in terms of its definiens). 