:: deftheorem defines terminal ALTCAT_3:def 10 :
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^> & <^o1,o^> is trivial ) );