:: deftheorem Def4 defines IdsMap YELLOW_2:def 4 :
for L being non empty Poset
for b₂ being Function of L,(InclPoset (Ids L)) holds
( b₂ = IdsMap L iff for x being Element of L holds b₂ . x = downarrow x );