:: deftheorem Def6 defines are_dual YELLOW18:def 6 :
for A, B being category holds
( A,B are_dual iff A,B opp are_equivalent );