:: deftheorem defines *id OPPCAT_1:def 13 :
for C being Category holds *id C = *' (id C);