theorem Th82: :: FILTER_2:82

for L being Lattice
for p, q being Element of L st p [= q holds
( latt (L,[#p,q#]) is bounded & Top (latt (L,[#p,q#])) = q & Bottom (latt (L,[#p,q#])) = p )