theorem :: CAT_1:49

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