:: deftheorem defines id CAT_1:def 24 :
for C being Category holds id C = id the carrier' of C;