Description: The successor of an ordinal number is an ordinal number. Closed form of
onsuci . Forward implication of onsucb . Proposition 7.24 of
TakeutiZaring p. 41. Remark 1.5 of Schloeder p. 1. (Contributed by NM, 6-Jun-1994)(Proof shortened by BTernaryTau, 30-Nov-2024)