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

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