\begin{definition}[Definition:Finite Ordinal]
Let $\alpha$ be an ordinal.
Then $\alpha$ is said to be '''finite''' {{iff}} one of the following holds:
:$\alpha = \O$
:$\alpha = \beta^+$ for some '''finite ordinal''' $\beta$
where $\O$ denotes the empty set, and $\beta^+$ is the successor ordinal of $\beta$.
\end{definition}