theorem :: YELLOW18:27

for A, B, C being category st A,B are_opposite holds
( A,C are_equivalent iff B,C are_dual )