Order Type

OT#PROP.

Every well-ordered set $W$ is isomorphic to a unique ordinal number.

OT#DEF.

This unique ordinal number is called the order type of $W$ (with respect to the given well-order).