Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: x0 ∈ omega. Apply nat_p_omega with ordsucc x0. Apply nat_ordsucc with x0. Apply omega_nat_p with x0. The subproof is completed by applying H0. ■