:: deftheorem defines initial ALTCAT_3:def 9 :
for C being AltGraph
for o being Object of C holds
( o is initial iff for o1 being Object of C ex M being Morphism of o,o1 st
( M in <^o,o1^> & <^o,o1^> is trivial ) );