Ordinal Class is Ordinal
Theorem
The Ordinal Class $\operatorname{On}$ is an ordinal.
Proof
All ordinals are not elements of themselves, since $\Epsilon$ is an ordering relation on the ordinal classes. That is:
$\forall A \in \operatorname{On}: A \not\in A$ (1)
However, the class of all ordinal numbers is an ordinal itself. Since for ordering relations on the ordinals, the membership relation is equivalent to the subset relation in all instances (see the definition of Ordinals), we have that:
$\forall x \in \operatorname{On}: x \subset \operatorname{On}$ (2)
The segment of the class of ordinals is:
{ $x \in \operatorname{On} | x \subset \operatorname{On}$ } (3)
Which, by (2) is equal to the $\operatorname{On}$. Therefore $\operatorname{On}$ is an Ordinal.
Please fix formatting and $\LaTeX$ errors and inconsistencies.
It may also need to be brought up to our standard house style.
If you have done this or know it has been done, please remove {{Tidy}} from the code.
