theorem :: OPPCAT_1:25

for C being Category
for c being Object of C holds
( c is initial iff c opp is terminal )