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