theorem :: FILTER_2:23

for L being Lattice
for I being Ideal of L ex p being Element of L st p in I