set C = OrdC 0;
take OrdC 0 ; :: thesis: ( OrdC 0 is strict & not OrdC 0 is terminal )
ex C1 being category st
for F being Functor of C1,(OrdC 0) holds
( not F is covariant or ex F1 being Functor of C1,(OrdC 0) st
( F1 is covariant & not F = F1 ) )

proof

take OrdC 1 ; :: thesis: for F being Functor of (OrdC 1),(OrdC 0) holds
( not F is covariant or ex F1 being Functor of (OrdC 1),(OrdC 0) st
( F1 is covariant & not F = F1 ) )
Mor (OrdC 0) = {} ;
hence for F being Functor of (OrdC 1),(OrdC 0) holds
( not F is covariant or ex F1 being Functor of (OrdC 1),(OrdC 0) st
( F1 is covariant & not F = F1 ) ) by CAT_6:31; :: thesis: verum

end;

hence ( OrdC 0 is strict & not OrdC 0 is terminal ) ; :: thesis: verum