let M be BimapStr of 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 by Def14;
then consider f being Function of the carrier of C1,the carrier of C2 such that
A1: the ObjectMap of M = ~ [:f,f:] by Def3;
(~ [:f,f:]) .: (id the carrier of C1) = [:f,f:] .: (id the carrier of C1) by Th4;
hence the ObjectMap of M .: (id the carrier of C1) c= id the carrier of C2 by A1, Th15; :: according to FUNCTOR0:def 9 :: thesis: verum