let a be Element of (TolCat X); :: according to CAT_1:def 10 :: thesis: ex b₁ being Morphism of a,a st
for b₂ being Element of the carrier of (TolCat X) holds
( ( Hom (a,b₂) = {} or for b₃ being Morphism of a,b₂ holds b₃ (*) b₁ = b₃ ) & ( Hom (b₂,a) = {} or for b₃ being Morphism of b₂,a holds b₁ (*) b₃ = b₃ ) )
reconsider aa = a as Element of TOL X ;
reconsider ii = id$ aa as Morphism of (TolCat X) ;
A1: cod ii = cod (id$ aa) by Def25
.= aa ;
dom ii = dom (id$ aa) by Def24
.= aa ;
then ii in Hom (a,a) by A1;
then reconsider ii = ii as Morphism of a,a by CAT_1:def 5;
take ii ; :: thesis: for b₁ being Element of the carrier of (TolCat X) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) ii = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds ii (*) b₂ = b₂ ) )
thus for b₁ being Element of the carrier of (TolCat X) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) ii = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds ii (*) b₂ = b₂ ) ) by Lm5; :: thesis: verum