let L be distributive Lattice; :: thesis: for F being Ideal of L st F is maximal holds
F is prime
let F be Ideal 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 Lem2;
set G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } ;
{ x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } or y in the carrier of L )
assume y in { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } ; :: thesis: y in the carrier of L
then consider x being Element of L such that
S2: ( y = x & ex u being Element of L st
( u in F & x [= a "\/" u ) ) ;
thus y in the carrier of L by S2; :: thesis: verum

end;

then reconsider G = { x where x is Element of L : ex u being Element of L st
( u in F & x [= a "\/" u ) } as Subset of L ;
set u = the Element of F;
a [= a "\/" the Element of F by LATTICES:5;
then ze: a in G ;
reconsider G = G as Ideal of L by HelpMaxPrime2, ze;
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 & x [= a "\/" m ) ) ;
consider c being Element of L such that
J2: ( c in F & b [= a "\/" c ) by J1;
c "/\" b in F by J2, FILTER_2:22;
then (a "/\" b) "\/" (c "/\" b) in F by FILTER_2:21, S1;
then (a "\/" c) "/\" b in F by LATTICES:def 11;
hence contradiction by S1, J2, LATTICES:4; :: 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 ;
vv [= a "\/" vv by LATTICES:5;
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, S1, ze; :: thesis: verum