:: deftheorem defines with_terminal_objects CAT_8:def 3 :
for C being category holds
( C is with_terminal_objects iff ex a being Object of C st a is terminal );