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 A1: ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D ) ; :: thesis: D is id-inheriting
reconsider D = D as non empty full SubCatStr of C by A1, Th34;

now

let o be object of D; :: thesis: for o' being object of C st o = o' holds
idm o' in <^o,o^>
let o' be object of C; :: thesis: ( o = o' implies idm o' in <^o,o^> )
assume A2: o = o' ; :: thesis: idm o' in <^o,o^>
<^o',o'^> = <^o,o^> by A2, ALTCAT_2:29;
hence idm o' in <^o,o^> ; :: thesis: verum

end;

hence D is id-inheriting by ALTCAT_2:def 14; :: thesis: verum