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:63, LATTICE2:78;
then {(Bottom L)} is Filter of (L .:) by FILTER_0:13;
hence {(Bottom L)} is Ideal of L by Th21; :: thesis: verum