let D be non empty SubCatStr of C; :: thesis: ( D is id-inheriting & D is transitive implies D is with_units )
assume that
A1: D is id-inheriting and
A2: D is transitive ; :: thesis: D is with_units
let o be object of ; :: according to ALTCAT_2:def 9 :: thesis: ( <^o,o^> <> {} & ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) )
reconsider p = o as object of by Th30;
reconsider i = idm p as Morphism of , by A1, Def14;
A3: idm p in <^o,o^> by A1, Def14;
hence <^o,o^> <> {} ; :: thesis: ex i being Morphism of , st
for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
take i ; :: thesis: for o' being object of
for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let o' be object of ; :: thesis: for m' being Morphism of ,
for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m' be Morphism of ,; :: thesis: for m'' being Morphism of , holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m'' be Morphism of ,; :: thesis: ( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )

hereby :: thesis: ( <^o,o'^> <> {} implies m'' * i = m'' )

reconsider p' = o' as object of by Th30;
assume A4: <^o',o^> <> {} ; :: thesis: i * m' = m'
then A5: <^p',p^> <> {} by Th32, XBOOLE_1:3;
reconsider n' = m' as Morphism of , by A4, Th34;
thus i * m' = (idm p) * n' by A2, A3, A4, Th33
.= m' by A5, ALTCAT_1:24 ; :: thesis: verum

end;

reconsider p' = o' as object of by Th30;
assume A6: <^o,o'^> <> {} ; :: thesis: m'' * i = m''
then A7: <^p,p'^> <> {} by Th32, XBOOLE_1:3;
reconsider n'' = m'' as Morphism of , by A6, Th34;
thus m'' * i = n'' * (idm p) by A2, A3, A6, Th33
.= m'' by A7, ALTCAT_1:def 19 ; :: thesis: verum