theorem :: ALTCAT_4:12

for C being category
for o1, o2 being Object of C st o1 is initial & o2 is terminal & <^o2,o1^> <> {} holds
( o2 is initial & o1 is terminal )