:: deftheorem defines pr1 CAT_8:def 20 :
for C1, C2 being category holds pr1 (C1,C2) = the categorical_product of C1,C2 `2_3 ;