theorem :: OPPCAT_1:68

for C being Category
for c being Object of (C opp) holds (Obj (*id C)) . c = opp c