:: deftheorem defines ->OrdC1 CAT_8:def 5 :
for C being category
for b₂ being covariant Functor of C,(OrdC 1) holds
( b₂ = C ->OrdC1 iff verum );