let F be Functor of C1,C2; :: thesis: ( F is contravariant implies F is reflexive )
assume F is contravariant ; :: thesis: F is reflexive
then reconsider F = F as Contravariant FunctorStr of C1,C2 by Def28;
F is reflexive ;
hence F is reflexive ; :: thesis: verum