for a being Ordinal holds ord-type a = a by ORDERS_1:88;