theorem :: ALTCAT_3:25

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^> & ( for M1 being Morphism of o,o1 st M1 in <^o,o1^> holds
M = M1 ) ) )