let L be Lattice; :: thesis: ( L is lower-bounded implies {(Bottom L)} is Ideal of L )
assume L is lower-bounded ; :: thesis: {(Bottom L)} is Ideal of L
then ( Top (L .:) = Bottom L & L .: is upper-bounded ) by LATTICE2:48, LATTICE2:61;
then {(Bottom L)} is Filter of (L .:) by FILTER_0:12;
hence {(Bottom L)} is Ideal of L by Th20; :: thesis: verum