:: deftheorem defines terminal CAT_1:def 18 :
for C being Category
for a being Object of C holds
( a is terminal iff for b being Object of C holds
( Hom (b,a) <> {} & ex f being Morphism of b,a st
for g being Morphism of b,a holds f = g ) );