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