:: deftheorem defines DenseElements LATSTONE:def 9 :
for L being lower-bounded Lattice holds DenseElements L = { a where a is Element of L : a * = Bottom L } ;