:: deftheorem Def4 defines -INF_category WAYBEL34:def 4 :
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 -INF_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 infs-preserving ) ) ) );