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 of C1,C2 by Def27;
F is reflexive ;
hence F is reflexive ; :: thesis: verum