theorem Th14: :: YELLOW18:14

for A, B being category st A,B are_opposite holds
(dualizing-func (A,B)) * (dualizing-func (B,A)) = id B