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 15 :: thesis: ( not Hom b,a = {} & ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂ )
consider f being Morphism of b,a;
thus Hom b,a <> {} by Th7; :: thesis: ex b₁ being Morphism of b,a st
for b₂ being Morphism of b,a holds b₁ = b₂
take f ; :: thesis: for b₁ being Morphism of b,a holds f = b₁
thus for b₁ being Morphism of b,a holds f = b₁ by Th6; :: thesis: verum