:: deftheorem Def10 defines supMap WAYBEL23:def 10 :
for L being non empty reflexive transitive RelStr
for S being non empty full SubRelStr of L
for b₃ being Function of (InclPoset (Ids S)),L holds
( b₃ = supMap S iff for I being Ideal of S holds b₃ . I = "\/" (I,L) );