let L be D_Lattice; :: thesis: for F being Filter of L holds

( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )

let F be Filter of L; :: thesis: ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )

( F in F_primeSet L iff ex F0 being Filter of L st

( F0 = F & F0 <> the carrier of L & F0 is prime ) ) ;

hence ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) ) ; :: thesis: verum

( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )

let F be Filter of L; :: thesis: ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) )

( F in F_primeSet L iff ex F0 being Filter of L st

( F0 = F & F0 <> the carrier of L & F0 is prime ) ) ;

hence ( F in F_primeSet L iff ( F <> the carrier of L & F is prime ) ) ; :: thesis: verum