:: deftheorem Def4 defines terminal CAT_8:def 4 :
for C being category holds
( C is terminal iff for B being category ex F being Functor of B,C st
( F is covariant & ( for G being Functor of B,C st G is covariant holds
F = G ) ) );