:: deftheorem defines OrdC CAT_7:def 15 :
for O being ordinal number holds OrdC O = the strict preorder b₁ -ordered category;