let L be distributive Lattice; :: thesis: for F being Filter of L st F is maximal holds
F is prime
let F be Filter of L; :: thesis: ( F is maximal implies F is prime )
assume a5: F is maximal ; :: thesis: F is prime
assume not F is prime ; :: thesis: contradiction
then consider a, b being Element of L such that
S1: ( a "\/" b in F & not a in F & not b in F ) by Lem1;
set G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } ;
set u = the Element of F;
a "/\" the Element of F [= a by LATTICES:6;
then ZE: a in { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } ;
then reconsider G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } as Filter of L by HelpMaxPrime;
HH: not b in G

proof

assume b in G ; :: thesis: contradiction
then consider x being Element of L such that
J1: ( x = b & ex m being Element of L st
( m in F & a "/\" m [= x ) ) ;
consider c being Element of L such that
J2: ( c in F & a "/\" c [= b ) by J1;
c "\/" b in F by J2, FILTER_0:10;
then (a "\/" b) "/\" (c "\/" b) in F by FILTER_0:8, S1;
then (a "/\" c) "\/" b in F by LATTICES:11;
hence contradiction by S1, J2; :: thesis: verum

end;

H1: F c= G

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in F or v in G )
assume H2: v in F ; :: thesis: v in G
then reconsider vv = v as Element of L ;
a "/\" vv [= vv by LATTICES:6;
hence v in G by H2; :: thesis: verum

end;

G <> the carrier of L by HH;
then G is proper by SUBSET_1:def 6;
hence contradiction by H1, a5, ZE, S1; :: thesis: verum