:: deftheorem Def6 defines LowerAdj WAYBEL34:def 6 :
for W being with_non-empty_element set
for b₂ being strict contravariant Functor of W -INF_category ,W -SUP_category holds
( b₂ = W LowerAdj iff ( ( for a being Object of (W -INF_category) holds b₂ . a = latt a ) & ( for a, b being Object of (W -INF_category) st <^a,b^> <> {} holds
for f being Morphism of a,b holds b₂ . f = LowerAdj (@ f) ) ) );