let L be Lattice; for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded
let I be Ideal of L; ( L is lower-bounded implies latt (L,I) is lower-bounded )
set b9 = the Element of (latt (L,I));
reconsider b = the Element of (latt (L,I)) as Element of L by Th68;
given c being Element of L such that A1:
for a being Element of L holds
( c "/\" a = c & a "/\" c = c )
; LATTICES:def 13 latt (L,I) is lower-bounded
A2:
H1( latt (L,I)) = I
by Th72;
c "/\" b = c
by A1;
then reconsider c9 = c as Element of (latt (L,I)) by A2, Th22;
take
c9
; LATTICES:def 13 for b1 being Element of the carrier of (latt (L,I)) holds
( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 )
let a9 be Element of (latt (L,I)); ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L by Th68;
thus c9 "/\" a9 =
c "/\" a
by Th73
.=
c9
by A1
; a9 "/\" c9 = c9
hence
a9 "/\" c9 = c9
; verum