theorem Th15: :: ALTCAT_4:15

for C1, C2 being non empty AltCatStr
for F being Contravariant FunctorStr over C1,C2 holds
( F is faithful iff for o1, o2 being Object of C1 holds Morph-Map (F,o2,o1) is one-to-one )