theorem Th80: :: FILTER_2:80

for L being Lattice
for p being Element of L st L is lower-bounded holds
( latt (L,(.p.>) is lower-bounded & Bottom (latt (L,(.p.>)) = Bottom L )