:: deftheorem Def2 defines Funct CAT_2:def 2 :
for C, D being Category
for b₃ being set holds
( b₃ = Funct (C,D) iff for x being set holds
( x in b₃ iff x is Functor of C,D ) );