theorem :: FILTER_2:24

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
Bottom L in I