let B be non empty subcategory of A; :: thesis: B is set-id-inheriting
let b be Object of B; :: according to YELLOW18:def 10 :: thesis: idm b = id (B -carrier_of b)
( b in the carrier of B & the carrier of B c= the carrier of A ) by ALTCAT_2:def 11;
then reconsider a = b as Object of A ;
thus idm b = idm a by ALTCAT_2:34
.= id (the_carrier_of a) by YELLOW18:def 10
.= id (the_carrier_of b) by ALTCAT_2:34 ; :: thesis: verum