:: deftheorem Def8 defines initial CAT_8:def 8 :
for C being category holds
( C is initial iff for C1 being category ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) ) );