Order Type

PROP-OT.

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

DEF-OT.

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