:: deftheorem Def6 defines PrimeFilters LATTICEA:def 5 :
for L being Lattice
for b₂ being Function holds
( b₂ = PrimeFilters L iff ( dom b₂ = the carrier of L & ( for a being Element of L holds b₂ . a = { F where F is Filter of L : ( F is prime & a in F ) } ) ) );