:: deftheorem defines initial CAT_8:def 6 :
for C being CategoryStr
for a being Object of C holds
( a is initial iff for b being Object of C holds
( Hom (a,b) <> {} & ex f being Morphism of a,b st
for g being Morphism of a,b holds f = g ) );