for L being lower-bounded sup-Semilattice
for S being non empty full SubRelStr of L st Bottom L in the carrier of S & the carrier of S is join-closed Subset of L holds
for x being Element of L holds (waybelow x) /\ the carrier of S is Ideal of S