:: deftheorem defines term CAT_4:def 9 :
for C being Cartesian_category
for a being Object of C
for b₃ being Morphism of a, [1] C holds
( b₃ = term a iff verum );