:: deftheorem Def16 defines DownMap WAYBEL_4:def 16 :
for L being Semilattice
for I being Ideal of L
for b₃ being Function of L,(InclPoset (Ids L)) holds
( b₃ = DownMap I iff for x being Element of L holds
( ( x <= sup I implies b₃ . x = (downarrow x) /\ I ) & ( not x <= sup I implies b₃ . x = downarrow x ) ) );