let L be Lattice; :: thesis: 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 ) )
let a be Element of L; :: thesis: for F being Filter of L holds
( F in (PrimeFilters L) . a iff ( F is prime & a in F ) )
let F be Filter of L; :: thesis: ( F in (PrimeFilters L) . a iff ( F is prime & a in F ) )

hereby :: thesis: ( F is prime & a in F implies F in (PrimeFilters L) . a )

assume F in (PrimeFilters L) . a ; :: thesis: ( F is prime & a in F )
then ex F0 being Filter of L st
( F0 = F & F0 is prime & a in F0 ) by Th17;
hence ( F is prime & a in F ) ; :: thesis: verum

end;

thus ( F is prime & a in F implies F in (PrimeFilters L) . a ) by Th17; :: thesis: verum