:: deftheorem Def12 defines baseMap WAYBEL23:def 12 :
for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for b₃ being Function of L,(InclPoset (Ids (subrelstr B))) holds
( b₃ = baseMap B iff for x being Element of L holds b₃ . x = (waybelow x) /\ B );