theorem ThB: :: LATSTONE:2
for L being 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 )