theorem :: WAYBEL23:56

for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L holds
( dom (baseMap B) = the carrier of L & rng (baseMap B) is Subset of (Ids (subrelstr B)) ) by FUNCT_2:def 1, YELLOW_1:1;