:: deftheorem defines <. FILTER_0:def 2 :
for L being Lattice
for p being Element of L holds <.p.) = { q where q is Element of L : p [= q } ;