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 Th82;
hence latt (L,(.p.>) is bounded ; :: thesis: verum