for A being category
for B being non empty subcategory of A holds B opp is subcategory of A opp