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;
now :: thesis: for o being Object of D
for 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;
hence D is id-inheriting by ALTCAT_2:def 14; :: thesis: verum