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