:: deftheorem defines pr1 CAT_2:def 10 :
for C, D being Category holds pr1 (C,D) = pr1 ( the carrier' of C, the carrier' of D);