for L being Lattice
for a being Element of L
for F being Filter of L holds
( F in (PrimeFilters L) . a iff ( F is prime & a in F ) )