let o, m be set ; :: thesis: for a being Object of (c1Cat (o,m)) holds a is terminal
let a be Object of (c1Cat (o,m)); :: thesis: a is terminal
let b be Object of (c1Cat (o,m)); :: according to CAT_1:def 18 :: thesis: ( not Hom (b,a) = {} & ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂ )
set f = the Morphism of b,a;
thus Hom (b,a) <> {} by Th5; :: thesis: ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂
take the Morphism of b,a ; :: thesis: for b₁ being Morphism of b,a holds the Morphism of b,a = b₁
thus for b₁ being Morphism of b,a holds the Morphism of b,a = b₁ by Th4; :: thesis: verum