let C1 be non empty transitive with_units AltCatStr ; :: thesis: for C2 being non empty with_units AltCatStr
for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive
let C2 be non empty with_units AltCatStr ; :: thesis: for F being Functor of C1,C2 st F is contravariant & F is onto holds
F is coreflexive
let F be Functor of C1,C2; :: thesis: ( F is contravariant & F is onto implies F is coreflexive )
assume A1: ( F is contravariant & F is onto ) ; :: thesis: F is coreflexive
then F is Contravariant by Def28;
hence F is coreflexive by A1, Th46; :: thesis: verum