:: deftheorem defines (. FILTER_2:def 7 :
for L being Lattice
for p being Element of L holds (.p.> = { q where q is Element of L : q [= p } ;