theorem Th5: :: OPPCAT_1:6

for C being Category
for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a))