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