let M be BimapStr of 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 by Def13;
then ex f being Function of the carrier of C1,the carrier of C2 st the ObjectMap of M = [:f,f:] by Def2;
hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by Th15; :: according to FUNCTOR0:def 9 :: thesis: verum