:: deftheorem defines init CAT_3:def 12 :
for C being Category
for a, b being Object of C st a is initial holds
for b₄ being Morphism of a,b holds
( b₄ = init (a,b) iff verum );