theorem :: FILTER_2:64

for L being Lattice
for p being Element of L holds [#p,p#] = {p}