:: deftheorem Def3 defines SupMap YELLOW_2:def 3 :
for L being non empty Poset
for b₂ being Function of (InclPoset (Ids L)),L holds
( b₂ = SupMap L iff for I being Ideal of L holds b₂ . I = sup I );