let L be Lattice; :: thesis: for p being Element of L st L is lower-bounded holds
latt L,(.p.> is bounded
let p be Element of L; :: thesis: ( L is lower-bounded implies latt L,(.p.> is bounded )
assume L is lower-bounded ; :: thesis: latt L,(.p.> is bounded
then latt L,(.p.> is lower-bounded upper-bounded Lattice by Th80, Th82;
hence latt L,(.p.> is bounded ; :: thesis: verum