Mor (OrdC 0) = {} ;
then reconsider C = OrdC 0 as empty strict category ;
for C1 being category ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) )

proof

let C1 be category; :: thesis: ex F being Functor of C,C1 st
( F is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
F = F1 ) )
set F = the covariant Functor of C,C1;
take the covariant Functor of C,C1 ; :: thesis: ( the covariant Functor of C,C1 is covariant & ( for F1 being Functor of C,C1 st F1 is covariant holds
the covariant Functor of C,C1 = F1 ) )
thus the covariant Functor of C,C1 is covariant ; :: thesis: for F1 being Functor of C,C1 st F1 is covariant holds
the covariant Functor of C,C1 = F1
let F1 be Functor of C,C1; :: thesis: ( F1 is covariant implies the covariant Functor of C,C1 = F1 )
assume F1 is covariant ; :: thesis: the covariant Functor of C,C1 = F1
thus the covariant Functor of C,C1 = F1 ; :: thesis: verum

end;

hence ( OrdC 0 is empty & OrdC 0 is initial ) ; :: thesis: verum