:: deftheorem defines ord-type ORDINAL6:def 4 :
for X being set holds ord-type X = order_type_of (RelIncl (On X));