theorem Th81: :: FILTER_2:81

for L being Lattice
for p being Element of L st L is lower-bounded holds
latt (L,(.p.>) is bounded by Th80;