theorem :: CAT_8:30

for C being CategoryStr
for b being Object of C holds
( b is initial iff for a being Object of C ex f being Morphism of b,a st Hom (b,a) = {f} )