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