theorem Th23: :: FILTER_0:23

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