theorem Th36: :: FUNCTOR0:36

for A, B being non empty transitive with_units AltCatStr
for F being reflexive feasible FunctorStr over A,B st F is bijective & F is coreflexive holds
F " is reflexive