theorem Th79: :: FILTER_2:79

for L being Lattice
for p being Element of L holds Top (latt (L,(.p.>)) = p