theorem :: OPPCAT_1:26

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