:: deftheorem Def10 defines set-id-inheriting YELLOW18:def 10 :
for C being category holds
( C is set-id-inheriting iff for a being Object of C holds idm a = id (the_carrier_of a) );