:: deftheorem defines init CAT_4:def 27 :
for C being Cocartesian_category
for a being Object of C
for b₃ being Morphism of EmptyMS C,a holds
( b₃ = init a iff verum );