let C be non empty with_units AltCatStr ; :: thesis: for D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds

D is id-inheriting

let D be SubCatStr of C; :: thesis: ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D implies D is id-inheriting )

assume ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D ) ; :: thesis: D is id-inheriting

then reconsider D = D as non empty full SubCatStr of C by Th34;

D is id-inheriting

let D be SubCatStr of C; :: thesis: ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D implies D is id-inheriting )

assume ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D ) ; :: thesis: D is id-inheriting

then reconsider D = D as non empty full SubCatStr of C by Th34;

now :: thesis: for o being Object of D

for o9 being Object of C st o = o9 holds

idm o9 in <^o,o^>

hence
D is id-inheriting
by ALTCAT_2:def 14; :: thesis: verumfor o9 being Object of C st o = o9 holds

idm o9 in <^o,o^>

let o be Object of D; :: thesis: for o9 being Object of C st o = o9 holds

idm o9 in <^o,o^>

let o9 be Object of C; :: thesis: ( o = o9 implies idm o9 in <^o,o^> )

assume o = o9 ; :: thesis: idm o9 in <^o,o^>

then <^o9,o9^> = <^o,o^> by ALTCAT_2:28;

hence idm o9 in <^o,o^> ; :: thesis: verum

end;idm o9 in <^o,o^>

let o9 be Object of C; :: thesis: ( o = o9 implies idm o9 in <^o,o^> )

assume o = o9 ; :: thesis: idm o9 in <^o,o^>

then <^o9,o9^> = <^o,o^> by ALTCAT_2:28;

hence idm o9 in <^o,o^> ; :: thesis: verum