:: deftheorem Def14 defines -ordered CAT_7:def 14 :
for O being ordinal number
for C being composable with_identities CategoryStr holds
( C is O -ordered iff RelOb C, RelIncl O are_isomorphic );