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