theorem :: WAYBEL23:57

for L being lower-bounded continuous sup-Semilattice
for B being with_bottom CLbasis of L
for x being set st x in rng (baseMap B) holds
x is Ideal of (subrelstr B)