theorem Th15: :: YELLOW18:15

for A, B being category st A,B are_opposite holds
dualizing-func (A,B) is bijective