theorem :: ALTCAT_3:27

for C being AltGraph
for o being Object of C holds
( o is terminal iff for o1 being Object of C ex M being Morphism of o1,o st
( M in <^o1,o^> & ( for M1 being Morphism of o1,o st M1 in <^o1,o^> holds
M = M1 ) ) )