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 D; :: according to ALTCAT_2:def 9 :: thesis: ( <^o,o^> <> {} & ex i being Morphism of o,o st
for o' being object of D
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) ) )
reconsider p = o as object of C by Th30;
A3: idm p in <^o,o^> by A1, Def14;
hence <^o,o^> <> {} ; :: thesis: ex i being Morphism of o,o st
for o' being object of D
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
reconsider i = idm p as Morphism of o,o by A1, Def14;
take i ; :: thesis: for o' being object of D
for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let o' be object of D; :: thesis: for m' being Morphism of o',o
for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m' be Morphism of o',o; :: thesis: for m'' being Morphism of o,o' holds
( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )
let m'' be Morphism of o,o'; :: thesis: ( ( <^o',o^> <> {} implies i * m' = m' ) & ( <^o,o'^> <> {} implies m'' * i = m'' ) )

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

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

end;

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