:: deftheorem Def2 defines -LowerMap WAYBEL35:def 2 :
for L being lower-bounded with_suprema Poset
for R being auxiliary(ii) Relation of L
for b₃ being Function of L,(InclPoset (LOWER L)) holds
( b₃ = R -LowerMap iff for x being Element of L holds b₃ . x = R -below x );