:: deftheorem Def14 defines id-inheriting ALTCAT_2:def 14 :
for C being non empty with_units AltCatStr
for D being SubCatStr of C holds
( ( not D is empty implies ( D is id-inheriting iff for o being Object of D
for o9 being Object of C st o = o9 holds
idm o9 in <^o,o^> ) ) & ( D is empty implies ( D is id-inheriting iff verum ) ) );