let W be with_non-empty_element set ; :: thesis: W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj
W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under (W LowerAdj) " by Th52, YELLOW20:51;
hence W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj by Th18; :: thesis: verum