theorem :: ORDINAL6:15

for a being Ordinal holds ord-type {a} = 1