:: deftheorem defines ord-type ORDINAL6:def 5 :
for X being ordinal-membered set holds ord-type X = order_type_of (RelIncl X);