let W be with_non-empty_element set ; :: thesis: W -INF_category ,W -SUP_category are_anti-isomorphic
take W LowerAdj ; :: according to FUNCTOR0:def 40 :: thesis: ( W LowerAdj is bijective & W LowerAdj is contravariant )
thus ( W LowerAdj is bijective & W LowerAdj is contravariant ) ; :: thesis: verum