let L be Lattice; 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; ( 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 )
; ( 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 )
hence W1:
latt (L,I) is lower-bounded
by LATTICES:def 13; Bottom (latt (L,I)) = Bottom L
for a9 being Element of (latt (L,I)) holds
( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
hence
Bottom (latt (L,I)) = Bottom L
by LATTICES:def 16, W1; verum