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:48, LATTICE2:61;
then Bottom L in I .: by FILTER_0:11;
hence Bottom L in I ; :: thesis: verum