consider C being strict preorder category such that

A1: ( 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 } ) by Th37;

take C ; :: thesis: ( C is strict & C is O -ordered & C is preorder )

thus ( C is strict & C is O -ordered & C is preorder ) by A1, WELLORD1:38; :: thesis: verum

A1: ( 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 } ) by Th37;

take C ; :: thesis: ( C is strict & C is O -ordered & C is preorder )

thus ( C is strict & C is O -ordered & C is preorder ) by A1, WELLORD1:38; :: thesis: verum