:: deftheorem defines pr1 CAT_8:def 14 :
for C being with_binary_products category
for c1, c2 being Object of C holds pr1 (c1,c2) = the categorical_product of c1,c2 `2_3 ;