:: deftheorem Def10 defines -UPS_category YELLOW21:def 10 :
for W being non empty set st not for w being Element of W holds w is empty holds
for b₂ being strict lattice-wise category holds
( b₂ = W -UPS_category iff ( ( for x being LATTICE holds
( x is Object of b₂ iff ( x is strict & x is complete & the carrier of x in W ) ) ) & ( for a, b being Object of b₂
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff f is directed-sups-preserving ) ) ) );