:: deftheorem Def15 defines Map2Rel WAYBEL_4:def 15 :
for L being lower-bounded sup-Semilattice
for b₂ being Function of (MonSet L),(InclPoset (Aux L)) holds
( b₂ = Map2Rel L iff for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = b₂ . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) );