:: deftheorem defines PFilters LATTICEA:def 2 :
for L being Lattice holds PFilters L = { F where F is Filter of L : F is prime } ;