:: deftheorem defines -carrier_of YELLOW18:def 9 :
for C being category
for a being Object of C holds C -carrier_of a = proj1 (idm a);