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