let F be Functor of C1,C2; :: thesis: ( F is covariant implies F is reflexive )
assume F is covariant ; :: thesis: F is reflexive
then reconsider F = F as Covariant FunctorStr over C1,C2 by Def26;
F is reflexive ;
hence F is reflexive ; :: thesis: verum