consider f being morphism of (OrdC 1) such that
A1: ( f is identity & Ob (OrdC 1) = {f} & Mor (OrdC 1) = {f} ) by Th15;
A2: the carrier of (OrdC 1) = {f} by A1, CAT_6:def 1;
for C1 being category ex F being Functor of C1,(OrdC 1) st
( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )

proof

let C1 be category; :: thesis: ex F being Functor of C1,(OrdC 1) st
( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )

per cases ( C1 is empty or not C1 is empty ) ;

suppose C1 is empty ; :: thesis: ex F being Functor of C1,(OrdC 1) st
( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )

then reconsider C2 = C1 as empty category ;
set F2 = the covariant Functor of C2,(OrdC 1);
reconsider F = the covariant Functor of C2,(OrdC 1) as Functor of C1,(OrdC 1) ;
take F ; :: thesis: ( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )
thus ( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) ) ; :: thesis: verum

end;

suppose not C1 is empty ; :: thesis: ex F being Functor of C1,(OrdC 1) st
( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )

then reconsider C2 = C1 as non empty category ;
set F2 = the covariant Functor of C2,(OrdC 1);
reconsider F = the covariant Functor of C2,(OrdC 1) as Functor of C1,(OrdC 1) ;
take F ; :: thesis: ( F is covariant & ( for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1 ) )
thus F is covariant ; :: thesis: for F1 being Functor of C1,(OrdC 1) st F1 is covariant holds
F = F1
let F1 be Functor of C1,(OrdC 1); :: thesis: ( F1 is covariant implies F = F1 )
assume F1 is covariant ; :: thesis: F = F1
for x1 being object st x1 in the carrier of C1 holds
F . x1 = F1 . x1

proof

let x1 be object ; :: thesis: ( x1 in the carrier of C1 implies F . x1 = F1 . x1 )
assume x1 in the carrier of C1 ; :: thesis: F . x1 = F1 . x1
then A3: ( F . x1 in {f} & F1 . x1 in {f} ) by A2, FUNCT_2:5;
hence F . x1 = f by TARSKI:def 1
.= F1 . x1 by A3, TARSKI:def 1 ;
:: thesis: verum

end;

hence F = F1 by FUNCT_2:12; :: thesis: verum

end;

end;

end;

hence ( not OrdC 1 is empty & OrdC 1 is terminal ) ; :: thesis: verum