consider f being morphism of (OrdC 1) such that
A1: ( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} ) by Th15;
A2: for a, b being Object of (OrdC 1)
for f1 being morphism of (OrdC 1) holds f1 is Morphism of a,b

proof

let a, b be Object of (OrdC 1); :: thesis: for f1 being morphism of (OrdC 1) holds f1 is Morphism of a,b
let f1 be morphism of (OrdC 1); :: thesis: f1 is Morphism of a,b
A3: dom f1 = f by A1, TARSKI:def 1
.= a by A1, TARSKI:def 1 ;
cod f1 = f by A1, TARSKI:def 1
.= b by A1, TARSKI:def 1 ;
then f1 in Hom (a,b) by A3, CAT_7:20;
hence f1 is Morphism of a,b by CAT_7:def 3; :: thesis: verum

end;

reconsider a1 = f as Object of (OrdC 1) by A1;
take a1 ; :: according to CAT_8:def 3 :: thesis: a1 is terminal
let b1 be Object of (OrdC 1); :: according to CAT_8:def 2 :: thesis: ( Hom (b1,a1) <> {} & ex f being Morphism of b1,a1 st
for g being Morphism of b1,a1 holds f = g )
b1 = a1 by A1, TARSKI:def 1;
hence Hom (b1,a1) <> {} ; :: thesis: ex f being Morphism of b1,a1 st
for g being Morphism of b1,a1 holds f = g
reconsider f1 = f as Morphism of b1,a1 by A2;
take f1 ; :: thesis: for g being Morphism of b1,a1 holds f1 = g
let g be Morphism of b1,a1; :: thesis: f1 = g
thus f1 = g by A1, TARSKI:def 1; :: thesis: verum