theorem :: FILTER_2:42

for L being Lattice
for I being Ideal of L st L is upper-bounded & Top L in I holds
( I = (.L.> & I = the carrier of L )