let O be Ordinal; :: thesis: order_type_of (RelIncl O) = O
( RelIncl O is well-ordering & RelIncl O, RelIncl O are_isomorphic ) by WELLORD1:38;
hence order_type_of (RelIncl O) = O by WELLORD2:def 2; :: thesis: verum