theorem :: WAYBEL34:55

for W being with_non-empty_element set holds W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj