let L be Lattice; :: thesis: for I being non empty ClosedSubset of L st L is lower-bounded & Bottom L in I holds
( latt (L,I) is lower-bounded & Bottom (latt (L,I)) = Bottom L )
let I be non empty ClosedSubset of L; :: thesis: ( L is lower-bounded & Bottom L in I implies ( latt (L,I) is lower-bounded & Bottom (latt (L,I)) = Bottom L ) )
set b9 = the Element of (latt (L,I));
reconsider b = the Element of (latt (L,I)) as Element of L by FILTER_2:68;
assume A0: ( L is lower-bounded & Bottom L in I ) ; :: thesis: ( latt (L,I) is lower-bounded & Bottom (latt (L,I)) = Bottom L )
set c = Bottom L;
reconsider c9 = Bottom L as Element of (latt (L,I)) by FILTER_2:72, A0;
ex c9 being Element of (latt (L,I)) st
for a9 being Element of (latt (L,I)) holds
( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )

proof

take c9 ; :: thesis: for a9 being Element of (latt (L,I)) holds
( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
let a9 be Element of (latt (L,I)); :: thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L by FILTER_2:68;
thus c9 "/\" a9 = (Bottom L) "/\" a by FILTER_2:73
.= c9 by A0 ; :: thesis: a9 "/\" c9 = c9
hence a9 "/\" c9 = c9 ; :: thesis: verum

end;

hence W1: latt (L,I) is lower-bounded by LATTICES:def 13; :: thesis: Bottom (latt (L,I)) = Bottom L
for a9 being Element of (latt (L,I)) holds
( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )

proof

let a9 be Element of (latt (L,I)); :: thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L by FILTER_2:68;
thus c9 "/\" a9 = (Bottom L) "/\" a by FILTER_2:73
.= c9 by A0 ; :: thesis: a9 "/\" c9 = c9
hence a9 "/\" c9 = c9 ; :: thesis: verum

end;

hence Bottom (latt (L,I)) = Bottom L by LATTICES:def 16, W1; :: thesis: verum