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