:: deftheorem defines reflexive FUNCTOR0:def 8 :
for A, B being 1-sorted
for F being BimapStr over A,B holds
( F is reflexive iff the ObjectMap of F .: (id the carrier of A) c= id the carrier of B );