theorem Th24: :: FILTER_0:24

for L being Lattice
for p being Element of L
for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)