let M be BimapStr over C1,C2; :: thesis: ( M is Covariant implies M is reflexive )
assume M is Covariant ; :: thesis: M is reflexive
then the ObjectMap of M is Covariant ;
then ex f being Function of the carrier of C1, the carrier of C2 st the ObjectMap of M = [:f,f:] ;
hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by Th14; :: according to FUNCTOR0:def 8 :: thesis: verum