let L be distributive bounded Lattice; :: thesis: ( L is Boolean iff for I being Ideal of L st I is proper & I is prime holds
I is maximal )
thus ( L is Boolean implies for I being Ideal of L st I is proper & I is prime holds
I is maximal ) :: thesis: ( ( for I being Ideal of L st I is proper & I is prime holds
I is maximal ) implies L is Boolean )

proof

assume YY: L is Boolean ; :: thesis: for I being Ideal of L st I is proper & I is prime holds
I is maximal
let I be Ideal of L; :: thesis: ( I is proper & I is prime implies I is maximal )
assume Y0: ( I is proper & I is prime ) ; :: thesis: I is maximal
for G being Ideal of L st G is proper & I c= G holds
I = G

proof

let G be Ideal of L; :: thesis: ( G is proper & I c= G implies I = G )
assume y1: ( G is proper & I c= G ) ; :: thesis: I = G
then y3: G <> the carrier of L by SUBSET_1:def 6;
then I <> (.L.> by y1;
then I is max-ideal by Y0, FILTER_2:57, YY;
hence I = G by FILTER_2:def 8, y1, y3; :: thesis: verum

end;

hence I is maximal by Y0; :: thesis: verum

end;

assume A1: for I being Ideal of L st I is proper & I is prime holds
I is maximal ; :: thesis: L is Boolean
assume not L is Boolean ; :: thesis: contradiction
then not L is complemented ;
then consider a being Element of L such that
A2: for b being Element of L holds not b is_a_complement_of a ;
set I0 = PseudoComplements a;
reconsider I0 = PseudoComplements a as Ideal of L ;
a "/\" (Bottom L) = Bottom L ;
then C2: Bottom L in I0 ;
set I1 = { x where x is Element of L : ex y being Element of L st
( y in I0 & x [= a "\/" y ) } ;
{ x where x is Element of L : ex y being Element of L st
( y in I0 & x [= a "\/" y ) } c= the carrier of L

proof

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

end;

then reconsider I1 = { x where x is Element of L : ex y being Element of L st
( y in I0 & x [= a "\/" y ) } as Subset of L ;
for p, q being Element of L st p [= q & q in I1 holds
p in I1

proof

let p, q be Element of L; :: thesis: ( p [= q & q in I1 implies p in I1 )
assume C0: ( p [= q & q in I1 ) ; :: thesis: p in I1
then consider x1 being Element of L such that
C1: ( x1 = q & ex y being Element of L st
( y in I0 & x1 [= a "\/" y ) ) ;
consider y being Element of L such that
CC: ( y in I0 & x1 [= a "\/" y ) by C1;
p [= a "\/" y by C1, C0, LATTICES:7, CC;
hence p in I1 by CC; :: thesis: verum

end;

then C1: I1 is initial ;
for p, q being Element of L st p in I1 & q in I1 holds
p "\/" q in I1

proof

let p, q be Element of L; :: thesis: ( p in I1 & q in I1 implies p "\/" q in I1 )
assume d0: ( p in I1 & q in I1 ) ; :: thesis: p "\/" q in I1
then consider x1 being Element of L such that
d1: ( x1 = p & ex y being Element of L st
( y in I0 & x1 [= a "\/" y ) ) ;
consider y1 being Element of L such that
e1: ( y1 in I0 & x1 [= a "\/" y1 ) by d1;
consider x2 being Element of L such that
d2: ( x2 = q & ex y being Element of L st
( y in I0 & x2 [= a "\/" y ) ) by d0;
consider y2 being Element of L such that
e2: ( y2 in I0 & x2 [= a "\/" y2 ) by d2;
HH: y1 "\/" y2 in I0 by LATTICES:def 25, e1, e2;
FF: (a "\/" y1) "\/" (a "\/" y2) = ((a "\/" y1) "\/" a) "\/" y2 by LATTICES:def 5
.= ((a "\/" a) "\/" y1) "\/" y2 by LATTICES:def 5
.= a "\/" (y1 "\/" y2) by LATTICES:def 5 ;
x1 "\/" x2 [= (a "\/" y1) "\/" (a "\/" y2) by FILTER_0:4, e1, e2;
hence p "\/" q in I1 by HH, d1, d2, FF; :: thesis: verum

end;

then CC: I1 is join-closed ;
a [= a "\/" (Bottom L) ;
then ZZ: a in I1 by C2;
then reconsider I1 = I1 as Ideal of L by C1, CC;
q1: I0 c= I1

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in I0 or t in I1 )
assume C0: t in I0 ; :: thesis: t in I1
then consider x1 being Element of L such that
C1: ( x1 = t & a "/\" x1 = Bottom L ) ;
x1 [= a "\/" x1 by LATTICES:5;
hence t in I1 by C1, C0; :: thesis: verum

end;

J1: not Top L in I1

proof

assume Top L in I1 ; :: thesis: contradiction
then consider x1 being Element of L such that
D1: ( x1 = Top L & ex y being Element of L st
( y in I0 & x1 [= a "\/" y ) ) ;
consider y being Element of L such that
D2: ( y in I0 & Top L [= a "\/" y ) by D1;
consider x2 being Element of L such that
C1: ( x2 = y & a "/\" x2 = Bottom L ) by D2;
y is_a_complement_of a by C1, D2;
hence contradiction by A2; :: thesis: verum

end;

set FF = <.(Top L).);
<.(Top L).) = [#(Top L),(Top L)#] by FILTER_2:65;
then J2: <.(Top L).) = {(Top L)} by FILTER_2:64;
then <.(Top L).) misses I1 by J1, ZFMISC_1:50;
then consider J0 being Ideal of L such that
B1: ( J0 is prime & I1 c= J0 & J0 misses <.(Top L).) ) by Th15;
S4: J0 <> the carrier of L by B1, ZFMISC_1:48, J2;
set T = the carrier of L;
reconsider D = the carrier of L \ J0 as non empty Subset of L by S4, XBOOLE_1:37;
for p, q being Element of L st p [= q & p in D holds
q in D

proof

let p, q be Element of L; :: thesis: ( p [= q & p in D implies q in D )
assume k0: ( p [= q & p in D ) ; :: thesis: q in D
then ( p in the carrier of L & not p in J0 ) by XBOOLE_0:def 5;
then not q in J0 by k0, FILTER_2:21;
hence q in D by XBOOLE_0:def 5; :: thesis: verum

end;

then j1: D is final ;
for p, q being Element of L st p in D & q in D holds
p "/\" q in D

proof

let p, q be Element of L; :: thesis: ( p in D & q in D implies p "/\" q in D )
assume ( p in D & q in D ) ; :: thesis: p "/\" q in D
then ( p in the carrier of L & not p in J0 & q in the carrier of L & not q in J0 ) by XBOOLE_0:def 5;
then not p "/\" q in J0 by FILTER_2:def 10, B1;
hence p "/\" q in D by XBOOLE_0:def 5; :: thesis: verum

end;

then zc: D is meet-closed ;
reconsider F = <.(<.a.) \/ D).) as Filter of L ;
a in <.a.) ;
then H1: a in <.a.) \/ D by XBOOLE_0:def 3;
h2: D \/ <.a.) c= F by FILTER_0:def 4;
G1: not the carrier of L c= J0 by B1, ZFMISC_1:48, J2;
then G2: the carrier of L \ J0 <> {} by XBOOLE_1:37;
D c= D \/ <.a.) by XBOOLE_1:7;
then mm: D c= F by h2;
F misses I0

proof

assume F meets I0 ; :: thesis: contradiction
then consider h being object such that
H1: ( h in F & h in I0 ) by XBOOLE_0:3;
consider x1 being Element of L such that
C1: ( x1 = h & a "/\" x1 = Bottom L ) by H1;
consider b being object such that
n1: b in the carrier of L \ J0 by XBOOLE_0:def 1, G2;
reconsider b = b as Element of L by n1;
consider bb being Element of L such that
m2: ( bb in D & a "/\" bb [= x1 ) by LATTICE4:3, zc, C1, H1, j1;
W1: ( bb "/\" a [= x1 & not bb in J0 ) by m2, XBOOLE_0:def 5;
bb "/\" a [= a by LATTICES:6;
then bb "/\" a = Bottom L by C1, BOOLEALG:9, m2, FILTER_0:7;
then bb in I0 ;
hence contradiction by W1, B1, q1; :: thesis: verum

end;

then consider J1 being Ideal of L such that
B2: ( J1 is prime & I0 c= J1 & J1 misses F ) by Th15;
J1 <> the carrier of L by H1, h2, B2, XBOOLE_0:3;
then S1: J1 is proper by SUBSET_1:def 6;
S2: J0 is proper by G1, SUBSET_1:def 6;
S3: J1 <> J0 by B1, ZZ, h2, H1, XBOOLE_0:3, B2;
J1 c= J0

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in J1 or t in J0 )
assume f3: t in J1 ; :: thesis: t in J0
then not t in D by mm, B2, XBOOLE_0:3;
hence t in J0 by f3, XBOOLE_0:def 5; :: thesis: verum

end;

then not J1 is maximal by S2, S3;
hence contradiction by B2, A1, S1; :: thesis: verum