let L be Lattice; :: thesis: for I being Ideal of L st L is lower-bounded holds
latt L,I is lower-bounded
let I be Ideal of L; :: thesis: ( L is lower-bounded implies latt L,I is lower-bounded )
given c being Element of L such that A1: for a being Element of L holds
( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def 13 :: thesis: latt L,I is lower-bounded
consider b' being Element of (latt L,I);
reconsider b = b' as Element of L by Th69;
( H₁( latt L,I) = I & c "/\" b = c ) by A1, Th73;
then reconsider c' = c as Element of (latt L,I) by Th23;
take c' ; :: according to LATTICES:def 13 :: thesis: for b₁ being Element of the carrier of (latt L,I) holds
( c' "/\" b₁ = c' & b₁ "/\" c' = c' )
let a' be Element of (latt L,I); :: thesis: ( c' "/\" a' = c' & a' "/\" c' = c' )
reconsider a = a' as Element of L by Th69;
thus c' "/\" a' = c "/\" a by Th74
.= c' by A1 ; :: thesis: a' "/\" c' = c'
hence a' "/\" c' = c' ; :: thesis: verum