:: deftheorem defines [x] CAT_8:def 19 :
for C1, C2 being category holds C1 [x] C2 = the categorical_product of C1,C2 `1_3 ;