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