let W be with_non-empty_element set ; :: thesis: W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj
set A1 = W -INF_category ;
set A2 = W -SUP_category ;
reconsider B1 = W -CL_category as non empty subcategory of W -INF_category by ALTCAT_4:36;
reconsider B2 = W -CL-opp_category as non empty subcategory of W -SUP_category by ALTCAT_4:36;
B2,B1 are_anti-isomorphic_under (W LowerAdj) " by Th54, YELLOW20:51;
hence W -CL-opp_category ,W -CL_category are_anti-isomorphic_under W UpperAdj by Th18; :: thesis: verum