:: deftheorem Def8 defines full CAT_5:def 8 :
for IT being Categorial Category holds
( IT is full iff for a, b being Category st a is Object of IT & b is Object of IT holds
for F being Functor of a,b holds [[a,b],F] is Morphism of IT );