let L be Lattice; :: thesis: for p being Element of L st {p} is Ideal of L holds
L is lower-bounded
let p be Element of L; :: thesis: ( {p} is Ideal of L implies L is lower-bounded )
assume {p} is Ideal of L ; :: thesis: L is lower-bounded
then {p} is Filter of (L .:) by Th20;
then L .: is upper-bounded by FILTER_0:13;
hence L is lower-bounded by LATTICE2:48; :: thesis: verum