:: deftheorem defines pr2 CAT_8:def 21 :
for C1, C2 being category holds pr2 (C1,C2) = the categorical_product of C1,C2 `3_3 ;