let L be distributive bounded Lattice; ( L is Boolean iff Spectrum L is unordered )
thus
( L is Boolean implies Spectrum L is unordered )
( Spectrum L is unordered implies L is Boolean )proof
assume
L is
Boolean
;
Spectrum L is unordered
then reconsider LL =
L as
Boolean Lattice ;
assume
not
Spectrum L is
unordered
;
contradiction
then consider P,
Q being
set such that F1:
(
P in Spectrum L &
Q in Spectrum L &
P <> Q &
P,
Q are_c=-comparable )
;
consider P1 being
Ideal of
L such that B1:
(
P1 = P &
P1 is
prime &
P1 is
proper )
by F1;
consider Q1 being
Ideal of
LL such that b1:
(
Q1 = Q &
Q1 is
prime &
Q1 is
proper )
by F1;
A2:
now not P c= Qassume f1:
P c= Q
;
contradictionthen
P c< Q
by F1;
then
Q \ P <> {}
by XBOOLE_1:105;
then consider a being
object such that A4:
a in Q \ P
by XBOOLE_0:def 1;
A5:
(
a in Q1 & not
a in P1 )
by b1, B1, A4, XBOOLE_0:def 5;
then reconsider a =
a as
Element of
LL ;
Q1 <> (.LL.>
by b1, SUBSET_1:def 6;
then
Q1 is
max-ideal
by FILTER_2:57, b1;
then B2:
not
a ` in P
by f1, b1, A4, FILTER_2:58;
a "/\" (a `) = Bottom LL
by LATTICES:20;
then
a "/\" (a `) in P
by FILTER_2:24, B1;
hence
contradiction
by B1, A5, B2, FILTER_2:def 10;
verum end;
now not Q c= Passume f1:
Q c= P
;
contradictionthen
Q c< P
by F1;
then
P \ Q <> {}
by XBOOLE_1:105;
then consider a being
object such that A4:
a in P \ Q
by XBOOLE_0:def 1;
A5:
(
a in P1 & not
a in Q1 )
by B1, b1, A4, XBOOLE_0:def 5;
then reconsider a =
a as
Element of
LL ;
P1 <> (.LL.>
by B1, SUBSET_1:def 6;
then
P1 is
max-ideal
by FILTER_2:57, B1;
then B2:
not
a ` in Q
by f1, B1, A4, FILTER_2:58;
a "/\" (a `) = Bottom LL
by LATTICES:20;
then
a "/\" (a `) in Q1
by FILTER_2:24;
hence
contradiction
by A5, B2, FILTER_2:def 10, b1;
verum end;
hence
contradiction
by A2, F1;
verum
end;
assume d1:
Spectrum L is unordered
; L is Boolean
assume
not L is Boolean
; contradiction
then
not L is complemented
;
then consider a being Element of L such that
C2:
for b being Element of L holds not b is_a_complement_of a
;
set D = PseudoCocomplements a;
reconsider D = PseudoCocomplements a as Filter of L ;
set D1 = <.(D \/ <.a.)).);
II:
<.(D \/ <.a.)).) = { r where r is Element of L : ex d, q being Element of L st
( d "/\" q [= r & d in D & q in <.a.) ) }
by FILTER_0:35;
AB:
<.(D \/ <.a.)).) c= { x where x is Element of L : ex d being Element of L st
( d in D & a "/\" d [= x ) }
{ x where x is Element of L : ex d being Element of L st
( d in D & a "/\" d [= x ) } c= <.(D \/ <.a.)).)
then Z0:
<.(D \/ <.a.)).) = { x where x is Element of L : ex d being Element of L st
( d in D & a "/\" d [= x ) }
by AB;
a "/\" the Element of D [= a
by LATTICES:6;
then HH:
a in <.(D \/ <.a.)).)
by Z0;
reconsider D1 = <.(D \/ <.a.)).) as Filter of L ;
HJ:
not Bottom L in D1
reconsider I0 = {(Bottom L)} as Ideal of L by FILTER_2:25;
consider P being Ideal of L such that
W0:
( P is prime & I0 c= P & P misses D1 )
by Th15, ZFMISC_1:50, HJ;
P <> the carrier of L
by W0, XBOOLE_0:3, HH;
then w0:
P is proper
by SUBSET_1:def 6;
set Pa = (.(P \/ (.a.>).>;
reconsider Pa = (.(P \/ (.a.>).> as Ideal of L ;
ZZ:
a in (.a.>
;
ZL:
P c= P \/ (.a.>
by XBOOLE_1:7;
ZK:
(.a.> c= P \/ (.a.>
by XBOOLE_1:7;
ZM:
P \/ (.a.> c= Pa
by FILTER_2:def 9;
kk:
D c= D \/ <.a.)
by XBOOLE_1:7;
D \/ <.a.) c= D1
by FILTER_0:def 4;
then hh:
D c= D1
by kk;
zx:
not a in P
by HH, W0, XBOOLE_0:3;
not Top L in Pa
then consider QQ being Ideal of L such that
W1:
( QQ is prime & Pa c= QQ & not Top L in QQ )
by Cor16;
QQ <> the carrier of L
by W1;
then w1:
QQ is proper
by SUBSET_1:def 6;
W2:
( P in Spectrum L & QQ in Spectrum L )
by W0, W1, w1, w0;
W3:
P <> QQ
by zx, W1, ZM, ZZ, ZK;
P c= QQ
by W1, ZL, ZM;
then
P,QQ are_c=-comparable
;
hence
contradiction
by d1, W2, W3; verum