theorem Th54: :: WAYBEL34:54
for W being with_non-empty_element set holds W -CL_category ,W -CL-opp_category are_anti-isomorphic_under W LowerAdj