let L be Lattice; :: thesis: for p being Element of st {p} is Ideal of L holds
L is lower-bounded
let p be Element of ; :: 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 Th21;
then L .: is upper-bounded by FILTER_0:14;
hence L is lower-bounded by LATTICE2:63; :: thesis: verum