theorem :: WAYBEL34:53

for W being with_non-empty_element set holds W -SUP(SO)_category ,W -INF(SC)_category are_anti-isomorphic_under W UpperAdj