theorem :: ORDERS_1:88

for O being Ordinal holds order_type_of (RelIncl O) = O