theorem :: ORDINAL6:17

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