:: deftheorem Def11 defines -SUP(SO)_category WAYBEL34:def 11 :
for W being with_non-empty_element set
for b₂ being non empty strict subcategory of W -SUP_category holds
( b₂ = W -SUP(SO)_category iff ( ( for a being Object of (W -SUP_category) holds a is Object of b₂ ) & ( for a, b being Object of (W -SUP_category)
for a9, b9 being Object of b₂ st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff UpperAdj (@ f) is directed-sups-preserving ) ) ) );