let L be Lattice; :: thesis: for I being Ideal of L st L is lower-bounded holds
Bottom L in I
let I be Ideal of L; :: thesis: ( L is lower-bounded implies Bottom L in I )
assume L is lower-bounded ; :: thesis: Bottom L in I
then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:63, LATTICE2:78;
then Bottom L in I .: by FILTER_0:12;
hence Bottom L in I ; :: thesis: verum