theorem Th37: :: CAT_7:37

for O being ordinal number ex C being strict preorder category st
( Ob C = O & ( for o1, o2 being Object of C st o1 in o2 holds
Hom (o1,o2) = {[o1,o2]} ) & RelOb C = RelIncl O & Mor C = O \/ { [o1,o2] where o1, o2 is Element of O : o1 in o2 } )