:: deftheorem defines --> CAT_2:def 1 :
for B, C being Category
for c being Object of C holds B --> c = the carrier' of B --> (id c);