:: deftheorem Def12 defines preorder CAT_7:def 12 :
for C being CategoryStr holds
( C is preorder iff for a, b being Object of C
for f1, f2 being morphism of C st f1 in Hom (a,b) & f2 in Hom (a,b) holds
f1 = f2 );