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