theorem :: FILTER_2:26

for L being Lattice
for p being Element of L st {p} is Ideal of L holds
L is lower-bounded