latticea.miz

    begin

    definition

      let IT be set;

      :: LATTICEA:def1

      attr IT is unordered means for p1,p2 be set st p1 in IT & p2 in IT & p1 <> p2 holds (p1,p2) are_c=-incomparable ;

    end

    registration

      cluster non trivial for B_Lattice;

      existence

      proof

        set L = { {} , { {} }};

        reconsider B = ( BooleLatt { {} }) as non empty LattStr;

        ( bool { {} }) = L by ZFMISC_1: 24;

        then

         A3: the carrier of B = L by LATTICE3:def 1;

         {} in L & { {} } in L by TARSKI:def 2;

        then B is non trivial by A3, ZFMISC_1:def 10;

        hence thesis;

      end;

    end

    theorem :: LATTICEA:1



     TopBot: for L be non trivial bounded Lattice holds ( Top L) <> ( Bottom L)

    proof

      let L be non trivial bounded Lattice;

      set p = ( Top L);

      assume

       A0: ( Top L) = ( Bottom L);

      consider p be Element of L such that

       A2: p <> ( Top L) by SUBSET_1: 50;

      ( Bottom L) [= p;

      hence thesis by A2, A0;

    end;

    theorem :: LATTICEA:2

    for L be Lattice, I be Ideal of L holds I is prime iff (I ` ) is Filter of L or (I ` ) = {}

    proof

      let L be Lattice, I be Ideal of L;

      set F = (I ` );

      thus I is prime implies (I ` ) is Filter of L or (I ` ) = {}

      proof

        assume I is prime;

        then

         A1: for x,y be Element of L st (x "/\" y) in I holds x in I or y in I by FILTER_2:def 10;



         A2: F is meet-closed

        proof

          let x,y be Element of L;

          assume x in F & y in F;

          then ( not x in I) & not y in I by XBOOLE_0:def 5;

          hence thesis by A1, SUBSET_1: 29;

        end;

        F is final

        proof

          let x,y be Element of L;

          assume that

           A5: x [= y and

           A4: x in F;

          y in I implies x in I by A5, LATTICES:def 22;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

        hence thesis by A2;

      end;

      assume

       A6: (I ` ) is Filter of L or (I ` ) = {} ;

      for x,y be Element of L holds (x "/\" y) in I iff x in I or y in I

      proof

        let x,y be Element of L;

        hereby

          assume (x "/\" y) in I;

          then

           T1: not (x "/\" y) in F by XBOOLE_0:def 5;

          per cases by A6;

            suppose F is Filter of L;

            then not x in F or not y in F by T1, FILTER_0: 9;

            hence x in I or y in I by XBOOLE_0:def 5;

          end;

            suppose

             T2: F = {} ;

            I = (F ` );

            hence x in I or y in I by T2;

          end;

        end;

        assume x in I or y in I;

        then

         T4: not x in F or not y in F by XBOOLE_0:def 5;

        per cases by A6;

          suppose F is Filter of L;

          then not (x "/\" y) in F by FILTER_0: 8, T4;

          hence (x "/\" y) in I by XBOOLE_0:def 5;

        end;

          suppose

           T2: F = {} ;

          I = (F ` );

          hence (x "/\" y) in I by T2;

        end;

      end;

      hence thesis by FILTER_2:def 10;

    end;

    theorem :: LATTICEA:3

    for L be Lattice, F be Filter of L holds F is prime iff (F ` ) is Ideal of L or (F ` ) = {}

    proof

      let L be Lattice, I be Filter of L;

      set F = (I ` );

      thus I is prime implies F is Ideal of L or F = {}

      proof

        assume I is prime;

        then

         A1: for x,y be Element of L st (x "\/" y) in I holds x in I or y in I by FILTER_0:def 5;



         A2: F is join-closed

        proof

          let x,y be Element of L;

          assume x in F & y in F;

          then ( not x in I) & not y in I by XBOOLE_0:def 5;

          hence thesis by A1, SUBSET_1: 29;

        end;

        F is initial

        proof

          let x,y be Element of L;

          assume that

           A5: x [= y and

           A4: y in F;

          x in I implies y in I by A5, LATTICES:def 23;

          hence thesis by A4, XBOOLE_0:def 5;

        end;

        hence thesis by A2;

      end;

      assume

       A6: (I ` ) is Ideal of L or (I ` ) = {} ;

      for x,y be Element of L holds (x "\/" y) in I iff x in I or y in I

      proof

        let x,y be Element of L;

        hereby

          assume (x "\/" y) in I;

          then

           T1: not (x "\/" y) in F by XBOOLE_0:def 5;

          per cases by A6;

            suppose F is Ideal of L;

            then not x in F or not y in F by T1, FILTER_2: 21;

            hence x in I or y in I by XBOOLE_0:def 5;

          end;

            suppose

             T2: F = {} ;

            I = (F ` );

            hence x in I or y in I by T2;

          end;

        end;

        assume x in I or y in I;

        then

         T4: not x in F or not y in F by XBOOLE_0:def 5;

        per cases by A6;

          suppose F is Ideal of L;

          then not (x "\/" y) in F by FILTER_2: 86, T4;

          hence (x "\/" y) in I by XBOOLE_0:def 5;

        end;

          suppose

           T2: F = {} ;

          I = (F ` );

          hence (x "\/" y) in I by T2;

        end;

      end;

      hence thesis by FILTER_0:def 5;

    end;

    definition

      let L be Lattice;

      :: LATTICEA:def2

      func PFilters L -> Subset-Family of L equals { F where F be Filter of L : F is prime };

      coherence

      proof

        set US = { F where F be Filter of L : F is prime };

        US c= ( bool the carrier of L)

        proof

          let x be object;

          assume x in US;

          then ex UF be Filter of L st UF = x & UF is prime;

          hence thesis;

        end;

        hence thesis;

      end;

    end



     IIsPrime: for L be Lattice holds (.L.> is prime

    proof

      let L be Lattice;

      set F = (.L.>;

      for p,q be Element of L holds (p "/\" q) in F iff p in F or q in F;

      hence thesis by FILTER_2:def 10;

    end;

    registration

      let L be Lattice;

      cluster (.L.> -> prime;

      coherence by IIsPrime;

    end

    theorem :: LATTICEA:4



     PrimFil: for L be distributive Lattice holds ( F_primeSet L) c< ( PFilters L)

    proof

      let L be distributive Lattice;



       A1: ( F_primeSet L) c= ( PFilters L)

      proof

        let x be object;

        assume x in ( F_primeSet L);

        then

        consider F be Filter of L such that

         A2: x = F & F <> the carrier of L & F is prime;

        thus thesis by A2;

      end;

       not <.L.) in ( F_primeSet L)

      proof

        assume <.L.) in ( F_primeSet L);

        then

        consider F be Filter of L such that

         B1: F = <.L.) & F <> the carrier of L & F is prime;

        thus thesis by B1;

      end;

      hence thesis by A1;

    end;

    begin

    theorem :: LATTICEA:5



     lemma3: the carrier of ( BooleLatt { {} }) = { {} , { {} }}

    proof

      the carrier of ( BooleLatt { {} }) = ( bool { {} }) by LATTICE3:def 1;

      hence thesis by ZFMISC_1: 24;

    end;

    theorem :: LATTICEA:6



     lemma1: for L be Lattice, A be Subset of L st L = ( BooleLatt { {} }) holds A = {} or A = { {} } or A = { {} , { {} }} or A = { { {} }}

    proof

      let L be Lattice, A be Subset of L;

      assume L = ( BooleLatt { {} });

      then

       A2: the carrier of L = ( bool { {} }) by LATTICE3:def 1;

      ( bool { {} }) = { {} , { {} }} by ZFMISC_1: 24;

      hence thesis by ZFMISC_1: 36, A2;

    end;

    theorem :: LATTICEA:7



     lemma2: for L be Lattice, A be Filter of L st L = ( BooleLatt { {} }) holds A = {} or A = { {} , { {} }} or A = { { {} }}

    proof

      let L be Lattice, A be Filter of L;

      assume

       A0: L = ( BooleLatt { {} });

      A <> { {} }

      proof

        assume

         Z0: A = { {} };

        reconsider b = { {} }, a = {} as Element of L by TARSKI:def 2, A0, lemma3;



         z1: ( { {} } /\ {} ) = (b "/\" a) by A0, LATTICE3: 1;

        b in A & a in A iff (b "/\" a) in A by FILTER_0: 8;

        hence thesis by z1, Z0, TARSKI:def 1;

      end;

      hence thesis by A0, lemma1;

    end;

    theorem :: LATTICEA:8

    for L be Lattice, A be Filter of L st L = ( BooleLatt { {} }) holds A = {( Top L)} or A = <.L.)

    proof

      let L be Lattice, A be Filter of L;

      assume

       A0: L = ( BooleLatt { {} });

      ( Top L) = { {} } by A0, LATTICE3: 4;

      then

      reconsider B = { { {} }} as Filter of L by FILTER_0: 12, A0;

      per cases by lemma2, A0;

        suppose A = {} ;

        hence thesis;

      end;

        suppose A = { {} , { {} }};

        hence thesis by lemma3, A0;

      end;

        suppose A = { { {} }};

        hence thesis by A0, LATTICE3: 4;

      end;

    end;

    theorem :: LATTICEA:9

    for L be non trivial Boolean Lattice, A be Filter of L st L = ( BooleLatt { {} }) & A = {( Top L)} holds A is prime

    proof

      let L be non trivial Boolean Lattice, A be Filter of L;

      assume

       A1: L = ( BooleLatt { {} }) & A = {( Top L)};

      for H be Filter of L st A c= H & H <> the carrier of L holds A = H

      proof

        let H be Filter of L;

        assume A c= H & H <> the carrier of L;

        then H = {} or H = { { {} }} by lemma3, A1, lemma2;

        hence thesis by A1, LATTICE3: 4;

      end;

      then A is being_ultrafilter by A1, FILTER_0:def 3;

      hence thesis by FILTER_0: 45;

    end;

    theorem :: LATTICEA:10

    for L be Lattice, A be Filter of L st L = ( BooleLatt { {} }) & A is being_ultrafilter holds A = {( Top L)}

    proof

      let L be Lattice, A be Filter of L;

      assume

       A0: L = ( BooleLatt { {} });

      assume

       Z1: A is being_ultrafilter;



       A1: ( Top L) = { {} } by A0, LATTICE3: 4;

      then

      reconsider B = { { {} }} as Filter of L by FILTER_0: 12, A0;



       Z2: not {} in A

      proof

        assume {} in A;

        then ( Bottom L) in A by A0, LATTICE3: 3;

        hence contradiction by Z1, LOPCLSET: 29, A0;

      end;

      A <> { {} , { {} }} by Z2, TARSKI:def 2;

      hence thesis by A1, lemma2, A0;

    end;

    begin

    theorem :: LATTICEA:11



     Th16: for L be Lattice, a be Element of L holds { F where F be Filter of L : F is prime & a in F } c= ( PFilters L)

    proof

      let L be Lattice, a be Element of L;

      let x be object;

      assume x in { F where F be Filter of L : F is prime & a in F };

      then ex UF be Filter of L st UF = x & UF is prime & a in UF;

      hence thesis;

    end;

    definition

      let L be Lattice;

      let F be Filter of L;

      :: LATTICEA:def3

      attr F is maximal means F is proper & for G be Filter of L st G is proper & F c= G holds F = G;

    end

    registration

      let L be Lattice;

      cluster maximal -> proper for Filter of L;

      coherence ;

    end

    registration

      let L be Lattice;

      cluster maximal -> being_ultrafilter for Filter of L;

      coherence

      proof

        let F be Filter of L;

        assume

         a0: F is maximal;

        for H be Filter of L st F c= H & H <> the carrier of L holds F = H

        proof

          let H be Filter of L;

          assume

           A2: F c= H & H <> the carrier of L;

          then H is proper by SUBSET_1:def 6;

          hence thesis by a0, A2;

        end;

        hence thesis by a0, SUBSET_1:def 6, FILTER_0:def 3;

      end;

      cluster being_ultrafilter -> maximal for Filter of L;

      coherence

      proof

        let F be Filter of L;

        assume

         a0: F is being_ultrafilter;

        then

         A0: F <> the carrier of L & for H be Filter of L st F c= H & H <> the carrier of L holds F = H by FILTER_0:def 3;

        for G be Filter of L st G is proper & F c= G holds F = G

        proof

          let G be Filter of L;

          assume

           A2: G is proper & F c= G;

          then G <> the carrier of L by SUBSET_1:def 6;

          hence thesis by a0, A2, FILTER_0:def 3;

        end;

        hence thesis by A0, SUBSET_1:def 6;

      end;

    end

    definition

      let L be Lattice;

      let I be Ideal of L;

      :: LATTICEA:def4

      attr I is maximal means I is proper & for J be Ideal of L st J is proper & I c= J holds I = J;

    end

    theorem :: LATTICEA:12



     LemM: for L be Lattice, I be Ideal of L holds I is max-ideal iff I is maximal

    proof

      let L be Lattice, I be Ideal of L;

      hereby

        assume

         A0: I is max-ideal;

        then

         a2: I <> the carrier of L by FILTER_2:def 8;

        for G be Ideal of L st G is proper & I c= G holds I = G

        proof

          let G be Ideal of L;

          assume

           B1: G is proper & I c= G;

          then G <> the carrier of L by SUBSET_1:def 6;

          hence thesis by FILTER_2:def 8, A0, B1;

        end;

        hence I is maximal by a2, SUBSET_1:def 6;

      end;

      assume

       A0: I is maximal;

      for J be Ideal of L st I c= J & J <> the carrier of L holds I = J

      proof

        let J be Ideal of L;

        assume

         B1: I c= J & J <> the carrier of L;

        then J is proper by SUBSET_1:def 6;

        hence thesis by A0, B1;

      end;

      hence thesis by A0, FILTER_2:def 8, SUBSET_1:def 6;

    end;

    registration

      let L be Lattice;

      cluster maximal -> max-ideal for Ideal of L;

      coherence by LemM;

      cluster max-ideal -> maximal for Ideal of L;

      coherence by LemM;

    end

    registration

      let L be Lattice;

      cluster maximal -> proper for Ideal of L;

      coherence ;

    end

    theorem :: LATTICEA:13



     Lem1: for L be Lattice, F be Filter of L st not F is prime holds ex a,b be Element of L st (a "\/" b) in F & not a in F & not b in F

    proof

      let L be Lattice, F be Filter of L;

      assume not F is prime;

      then

      consider a,b be Element of L such that

       Z1: not ((a "\/" b) in F iff a in F or b in F) by FILTER_0:def 5;

      now

        assume not (a "\/" b) in F & (a in F or b in F);

        per cases ;

          suppose not (a "\/" b) in F & a in F;

          hence contradiction by FILTER_0: 10;

        end;

          suppose not (a "\/" b) in F & b in F;

          hence contradiction by FILTER_0: 10;

        end;

      end;

      hence thesis by Z1;

    end;

    theorem :: LATTICEA:14



     Lem2: for L be Lattice, F be Ideal of L st not F is prime holds ex a,b be Element of L st (a "/\" b) in F & not a in F & not b in F

    proof

      let L be Lattice, F be Ideal of L;

      assume not F is prime;

      then

      consider a,b be Element of L such that

       Z1: not ((a "/\" b) in F iff a in F or b in F) by FILTER_2:def 10;

      now

        assume not (a "/\" b) in F & (a in F or b in F);

        per cases ;

          suppose not (a "/\" b) in F & a in F;

          hence contradiction by FILTER_2: 22;

        end;

          suppose not (a "/\" b) in F & b in F;

          hence contradiction by FILTER_2: 22;

        end;

      end;

      hence thesis by Z1;

    end;

    theorem :: LATTICEA:15



     HelpMaxPrime: for L be Lattice, F be Filter of L, a be Element of L, G be set st G = { x where x be Element of L : ex u be Element of L st u in F & (a "/\" u) [= x } & a in G holds G is Filter of L

    proof

      let L be Lattice;

      let F be Filter of L;

      let a be Element of L;

      let G be set;

      assume

       A1: G = { x where x be Element of L : ex u be Element of L st u in F & (a "/\" u) [= x } & a in G;

      G c= the carrier of L

      proof

        let y be object;

        assume y in G;

        then

        consider x be Element of L such that

         S2: y = x & ex u be Element of L st u in F & (a "/\" u) [= x by A1;

        thus thesis by S2;

      end;

      then

      reconsider G1 = G as Subset of L;

      set u = the Element of F;



       ZD: G1 is meet-closed

      proof

        let p,q be Element of L;

        assume

         P0: p in G1 & q in G1;

        then

        consider xx be Element of L such that

         P1: xx = p & ex u be Element of L st u in F & (a "/\" u) [= xx by A1;

        consider u1 be Element of L such that

         P3: u1 in F & (a "/\" u1) [= p by P1;

        consider yy be Element of L such that

         P2: yy = q & ex u be Element of L st u in F & (a "/\" u) [= yy by P0, A1;

        consider u2 be Element of L such that

         P4: u2 in F & (a "/\" u2) [= q by P2;



         P6: ((a "/\" u1) "/\" (a "/\" u2)) [= (p "/\" q) by P3, P4, FILTER_0: 5;



         P7: (u1 "/\" u2) in F by P3, P4, FILTER_0: 8;

        ((a "/\" u1) "/\" (a "/\" u2)) = (((a "/\" u1) "/\" a) "/\" u2) by LATTICES:def 7

        .= (((a "/\" a) "/\" u1) "/\" u2) by LATTICES:def 7

        .= (a "/\" (u1 "/\" u2)) by LATTICES:def 7;

        hence thesis by P7, P6, A1;

      end;

      G1 is final

      proof

        let p,q be Element of L;

        assume

         Y0: p [= q & p in G1;

        then

        consider s be Element of L such that

         Y1: s = p & ex u be Element of L st u in F & (a "/\" u) [= s by A1;

        consider u be Element of L such that

         Y2: u in F & (a "/\" u) [= s by Y1;

        (a "/\" u) [= q by Y2, Y0, Y1, LATTICES: 7;

        hence thesis by Y2, A1;

      end;

      hence thesis by A1, ZD;

    end;

    theorem :: LATTICEA:16



     HelpMaxPrime2: for L be Lattice, F be Ideal of L, a be Element of L, G be set st G = { x where x be Element of L : ex u be Element of L st u in F & x [= (a "\/" u) } & a in G holds G is Ideal of L

    proof

      let L be Lattice;

      let F be Ideal of L;

      let a be Element of L;

      let G be set;

      assume

       A1: G = { x where x be Element of L : ex u be Element of L st u in F & x [= (a "\/" u) } & a in G;

      G c= the carrier of L

      proof

        let y be object;

        assume y in G;

        then

        consider x be Element of L such that

         S2: y = x & ex u be Element of L st u in F & x [= (a "\/" u) by A1;

        thus thesis by S2;

      end;

      then

      reconsider G as Subset of L;

      set u = the Element of F;



       ZD: G is join-closed

      proof

        let p,q be Element of L;

        assume

         P0: p in G & q in G;

        then

        consider xx be Element of L such that

         P1: xx = p & ex u be Element of L st u in F & xx [= (a "\/" u) by A1;

        consider u1 be Element of L such that

         P3: u1 in F & p [= (a "\/" u1) by P1;

        consider yy be Element of L such that

         P2: yy = q & ex u be Element of L st u in F & yy [= (a "\/" u) by P0, A1;

        consider u2 be Element of L such that

         P4: u2 in F & q [= (a "\/" u2) by P2;



         P6: (p "\/" q) [= ((a "\/" u1) "\/" (a "\/" u2)) by P3, P4, FILTER_0: 4;



         P7: (u1 "\/" u2) in F by P3, P4, FILTER_2: 86;

        ((a "\/" u1) "\/" (a "\/" u2)) = (((a "\/" u1) "\/" a) "\/" u2) by LATTICES:def 5

        .= (((a "\/" a) "\/" u1) "\/" u2) by LATTICES:def 5

        .= (a "\/" (u1 "\/" u2)) by LATTICES:def 5;

        hence thesis by P7, P6, A1;

      end;

      G is initial

      proof

        let p,q be Element of L;

        assume

         Y0: p [= q & q in G;

        then

        consider s be Element of L such that

         Y1: s = q & ex u be Element of L st u in F & s [= (a "\/" u) by A1;

        consider u be Element of L such that

         Y2: u in F & s [= (a "\/" u) by Y1;

        p [= (a "\/" u) by Y2, Y0, Y1, LATTICES: 7;

        hence thesis by Y2, A1;

      end;

      hence thesis by ZD, A1;

    end;

    theorem :: LATTICEA:17



     MaxPrime: for L be distributive Lattice, F be Filter of L st F is maximal holds F is prime

    proof

      let L be distributive Lattice, F be Filter of L;

      assume

       a5: F is maximal;

      assume not F is prime;

      then

      consider a,b be 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 be Element of L : ex u be Element of L st u in F & (a "/\" u) [= x };

      set u = the Element of F;

      (a "/\" u) [= a by LATTICES: 6;

      then

       ZE: a in G;

      then

      reconsider G as Filter of L by HelpMaxPrime;



       HH: not b in G

      proof

        assume b in G;

        then

        consider x be Element of L such that

         J1: x = b & ex m be Element of L st m in F & (a "/\" m) [= x;

        consider c be 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 thesis by S1, J2;

      end;



       H1: F c= G

      proof

        let v be object;

        assume

         H2: v in F;

        then

        reconsider vv = v as Element of L;

        (a "/\" vv) [= vv by LATTICES: 6;

        hence thesis by H2;

      end;

      G <> the carrier of L by HH;

      then G is proper by SUBSET_1:def 6;

      hence thesis by H1, a5, ZE, S1;

    end;

    registration

      let L be distributive Lattice;

      cluster maximal -> prime for Filter of L;

      coherence by MaxPrime;

    end

    theorem :: LATTICEA:18



     MaxIPrime: for L be distributive Lattice, F be Ideal of L st F is maximal holds F is prime

    proof

      let L be distributive Lattice, F be Ideal of L;

      assume

       a5: F is maximal;

      assume not F is prime;

      then

      consider a,b be 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 be Element of L : ex u be Element of L st u in F & x [= (a "\/" u) };

      G c= the carrier of L

      proof

        let y be object;

        assume y in G;

        then

        consider x be Element of L such that

         S2: y = x & ex u be Element of L st u in F & x [= (a "\/" u);

        thus thesis by S2;

      end;

      then

      reconsider G as Subset of L;

      set u = the Element of F;

      a [= (a "\/" u) by LATTICES: 5;

      then

       ze: a in G;

      reconsider G as Ideal of L by HelpMaxPrime2, ze;



       HH: not b in G

      proof

        assume b in G;

        then

        consider x be Element of L such that

         J1: x = b & ex m be Element of L st m in F & x [= (a "\/" m);

        consider c be 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 thesis by S1, J2, LATTICES: 4;

      end;



       H1: F c= G

      proof

        let v be object;

        assume

         H2: v in F;

        then

        reconsider vv = v as Element of L;

        vv [= (a "\/" vv) by LATTICES: 5;

        hence thesis by H2;

      end;

      G <> the carrier of L by HH;

      then G is proper by SUBSET_1:def 6;

      hence thesis by H1, a5, S1, ze;

    end;

    registration

      let L be distributive Lattice;

      cluster maximal -> prime for Ideal of L;

      coherence by MaxIPrime;

    end

    begin

    ::$Notion-Name

    theorem :: LATTICEA:19



     Th15: for L be distributive Lattice, I be Ideal of L, F be Filter of L st I misses F holds ex P be Ideal of L st P is prime & I c= P & P misses F

    proof

      let L be distributive Lattice, I be Ideal of L, F be Filter of L;

      assume

       A1: I misses F;

      set X = { i where i be Ideal of L : I c= i & i misses F };



       z1: I in X by A1;

      for Z be set st Z <> {} & Z c= X & Z is c=-linear holds ( union Z) in X

      proof

        let Z be set;

        assume

         s1: Z <> {} & Z c= X & Z is c=-linear;



         BB: for x be object st x in Z holds x is Ideal of L

        proof

          let x be object;

          assume x in Z;

          then x in X by s1;

          then

          consider i be Ideal of L such that

           SO: i = x & I c= i & i misses F;

          thus thesis by SO;

        end;

        set M = ( union Z);

        consider f be object such that

         K1: f in Z by s1, XBOOLE_0:def 1;

        reconsider f as set by TARSKI: 1;



         UU: M c= the carrier of L

        proof

          let x be object;

          assume x in M;

          then

          consider g be set such that

           U1: x in g & g in Z by TARSKI:def 4;

          g is Ideal of L by U1, BB;

          hence thesis by U1;

        end;

        f in X by K1, s1;

        then

        consider j be Ideal of L such that

         SF: f = j & I c= j & j misses F;

        f c= M by K1, ZFMISC_1: 74;

        then

        reconsider M as non empty Subset of L by SF, UU;

         H0:

        now

          let a,b be Element of L;

          assume

           S1: a in M & b in M;

          then

          consider W be set such that

           S2: a in W & W in Z by TARSKI:def 4;

          consider V be set such that

           S3: b in V & V in Z by S1, TARSKI:def 4;



           H1: V is Ideal of L by S3, BB;



           h1: W is Ideal of L by S2, BB;

          (W,V) are_c=-comparable by s1, S2, S3, ORDINAL1:def 8;

          per cases ;

            suppose W c= V;

            then

             H2: (a "\/" b) in V by FILTER_2: 21, H1, S2, S3;

            V c= M by ZFMISC_1: 74, S3;

            hence (a "\/" b) in M by H2;

          end;

            suppose V c= W;

            then

             H2: (a "\/" b) in W by FILTER_2: 21, h1, S2, S3;

            W c= M by ZFMISC_1: 74, S2;

            hence (a "\/" b) in M by H2;

          end;

        end;

        for p,q be Element of L st p in M & q [= p holds q in M

        proof

          let p,q be Element of L;

          assume

           J0: p in M & q [= p;

          then

          consider W be set such that

           J1: p in W & W in Z by TARSKI:def 4;

          W is Ideal of L by J1, BB;

          then q in W by FILTER_2: 21, J0, J1;

          hence q in M by TARSKI:def 4, J1;

        end;

        then

         F2: M is Ideal of L by H0, FILTER_2: 21;



         F1: I c= M

        proof

          let t be object;

          assume

           J1: t in I;

          consider J be object such that

           SS: J in Z by s1, XBOOLE_0:def 1;

          J in X by SS, s1;

          then

          consider j be Ideal of L such that

           SF: j = J & I c= j & j misses F;

          thus thesis by SS, TARSKI:def 4, J1, SF;

        end;

        M misses F

        proof

          assume M meets F;

          then

          consider x be object such that

           F4: x in M & x in F by XBOOLE_0: 3;

          reconsider x as set by TARSKI: 1;

          consider y be set such that

           F5: x in y & y in Z by TARSKI:def 4, F4;

          y in X by F5, s1;

          then

          consider i be Ideal of L such that

           F6: i = y & I c= i & i misses F;

          thus thesis by F6, XBOOLE_0: 3, F4, F5;

        end;

        hence thesis by F1, F2;

      end;

      then

      consider Y be set such that

       J0: Y in X & for Z be set st Z in X & Z <> Y holds not Y c= Z by ORDERS_1: 67, z1;

      consider i be Ideal of L such that

       KK: Y = i & I c= i & i misses F by J0;

      take i;

      i is prime

      proof

        assume not i is prime;

        then

        consider a,b be Element of L such that

         G3: (a "/\" b) in i & not a in i & not b in i by Lem2;

        set Ia = (i "\/" (.a.>);

        i c= Ia by FILTER_2: 50;

        then

         J1: I c= Ia by KK;

        Ia meets F

        proof

          assume Ia misses F;

          then Ia in X by J1;

          then

           UI: Ia = i by FILTER_2: 50, J0, KK;

           (.a.> c= Ia by FILTER_2: 50;

          hence thesis by G3, UI, FILTER_2: 28;

        end;

        then

        consider p1 be object such that

         HH: p1 in Ia & p1 in F by XBOOLE_0: 3;

        reconsider p1 as Element of L by HH;

        consider p,q be Element of L such that

         h1: p1 = (p "\/" q) & p in i & q in (.a.> by HH;

        (p "\/" q) [= (p "\/" a) by FILTER_0: 1, FILTER_2: 28, h1;

        then (p "\/" a) in F by FILTER_0: 9, HH, h1;

        then

        consider p be Element of L such that

         G1: p in i & (p "\/" a) in F by h1;

        set Ib = (i "\/" (.b.>);

        i c= Ib by FILTER_2: 50;

        then

         J1: I c= Ib by KK;

        Ib meets F

        proof

          assume Ib misses F;

          then Ib in X by J1;

          then

           UI: Ib = i by FILTER_2: 50, J0, KK;

           (.b.> c= Ib by FILTER_2: 50;

          hence thesis by G3, UI, FILTER_2: 28;

        end;

        then

        consider p1 be object such that

         HH: p1 in Ib & p1 in F by XBOOLE_0: 3;

        reconsider p1 as Element of L by HH;

        consider P,Q be Element of L such that

         h1: p1 = (P "\/" Q) & P in i & Q in (.b.> by HH;

        (P "\/" Q) [= (P "\/" b) by FILTER_0: 1, FILTER_2: 28, h1;

        then (P "\/" b) in F by FILTER_0: 9, HH, h1;

        then

        consider q be Element of L such that

         G2: q in i & (q "\/" b) in F by h1;

        set y = ((p "\/" a) "/\" (q "\/" b));



         Z1: y in F by G1, G2, FILTER_0: 8;



         ZZ: y = (((p "\/" a) "/\" q) "\/" ((p "\/" a) "/\" b)) by LATTICES:def 11

        .= (((p "/\" q) "\/" (a "/\" q)) "\/" ((p "\/" a) "/\" b)) by LATTICES:def 11

        .= (((p "/\" q) "\/" (a "/\" q)) "\/" ((p "/\" b) "\/" (a "/\" b))) by LATTICES:def 11

        .= ((((p "/\" q) "\/" (a "/\" q)) "\/" (p "/\" b)) "\/" (a "/\" b)) by LATTICES:def 5

        .= ((((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b)) by LATTICES:def 5;

        set x = ((((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) "\/" (a "/\" b));



         G4: (p "/\" q) in i by G2, FILTER_2: 22;



         G5: (p "/\" b) in i by G1, FILTER_2: 22;



         G6: (a "/\" q) in i by G2, FILTER_2: 22;

        ((p "/\" q) "\/" (p "/\" b)) in i by G4, G5, FILTER_2: 21;

        then (((p "/\" q) "\/" (p "/\" b)) "\/" (a "/\" q)) in i by G6, FILTER_2: 21;

        then x in i by FILTER_2: 21, G3;

        hence thesis by KK, XBOOLE_0: 3, Z1, ZZ;

      end;

      hence thesis by KK;

    end;

    theorem :: LATTICEA:20



     Cor16: for L be distributive Lattice, I be Ideal of L, a be Element of L st not a in I holds ex P be Ideal of L st P is prime & I c= P & not a in P

    proof

      let L be distributive Lattice, I be Ideal of L, a be Element of L;

      assume

       A0: not a in I;

      set F = <.a.);



       A2: a in F;

      I misses F

      proof

        assume I meets F;

        then

        consider x be object such that

         A1: x in I & x in F by XBOOLE_0: 3;

        reconsider x as Element of L by A1;

        a [= x by A1, FILTER_0: 15;

        hence thesis by A0, FILTER_2: 21, A1;

      end;

      then

      consider P be Ideal of L such that

       T1: P is prime & I c= P & P misses F by Th15;

       not a in P by A2, T1, XBOOLE_0: 3;

      hence thesis by T1;

    end;

    theorem :: LATTICEA:21

    for L be distributive Lattice, a,b be Element of L st a <> b holds ex P be Ideal of L st P is prime & (a in P & not b in P) or ( not a in P & b in P)

    proof

      let L be distributive Lattice, a,b be Element of L;

      assume

       AA: a <> b;



       ZZ: (.a.> misses <.b.) or <.a.) misses (.b.>

      proof

        assume

         A0: (.a.> meets <.b.) & <.a.) meets (.b.>;

        then

        consider x be object such that

         A1: x in (.a.> & x in <.b.) by XBOOLE_0: 3;

        consider y be object such that

         A2: y in (.b.> & y in <.a.) by A0, XBOOLE_0: 3;

        reconsider x, y as Element of L by A1, A2;



         A3: x [= a by A1, FILTER_2: 28;

        b [= x by A1, FILTER_0: 15;

        then

         A5: b [= a by A3, LATTICES: 7;



         A4: y [= b by A2, FILTER_2: 28;

        a [= y by A2, FILTER_0: 15;

        then a [= b by A4, LATTICES: 7;

        hence thesis by AA, A5, LATTICES: 8;

      end;

      set I = (.a.>, F = <.b.);

      set I1 = (.b.>, F1 = <.a.);

      per cases by ZZ;

        suppose I misses F;

        then

        consider P be Ideal of L such that

         B1: P is prime & I c= P & P misses F by Th15;



         B2: a in P by B1, FILTER_2: 28;

        b in F;

        then not b in P by B1, XBOOLE_0: 3;

        hence thesis by B1, B2;

      end;

        suppose I1 misses F1;

        then

        consider P be Ideal of L such that

         B1: P is prime & I1 c= P & P misses F1 by Th15;



         B2: b in P by B1, FILTER_2: 28;

        a in F1;

        then not a in P by B1, XBOOLE_0: 3;

        hence thesis by B2;

      end;

    end;

    theorem :: LATTICEA:22

    for L be distributive Lattice, a,b be Element of L st not a [= b holds ex P be Ideal of L st P is prime & not a in P & b in P

    proof

      let L be distributive Lattice, a,b be Element of L;

      assume

       AA: not a [= b;



       ZZ: <.a.) misses (.b.>

      proof

        assume <.a.) meets (.b.>;

        then

        consider y be object such that

         A2: y in (.b.> & y in <.a.) by XBOOLE_0: 3;

        reconsider y as Element of L by A2;



         A4: y [= b by A2, FILTER_2: 28;

        a [= y by A2, FILTER_0: 15;

        hence thesis by AA, A4, LATTICES: 7;

      end;

      set I1 = (.b.>, F1 = <.a.);

      consider P be Ideal of L such that

       B1: P is prime & I1 c= P & P misses F1 by Th15, ZZ;



       B2: b in P by B1, FILTER_2: 28;

      a in F1;

      then not a in P by B1, XBOOLE_0: 3;

      hence thesis by B1, B2;

    end;

    theorem :: LATTICEA:23

    for L be distributive Lattice, I be Ideal of L holds I = ( meet { P where P be Ideal of L : P is prime & I c= P })

    proof

      let L be distributive Lattice, I be Ideal of L;



       X1: ( [#] L) is prime

      proof

        set II = ( [#] L);

        for p,q be Element of L holds (p "/\" q) in II iff p in II or q in II;

        hence thesis by FILTER_2:def 10;

      end;

      set P = ( [#] L);

      set X = { P where P be Ideal of L : P is prime & I c= P };

      set I1 = ( meet X);



       k1: P in X by X1;

      set x = the Element of X;

      ( meet X) c= the carrier of L by k1, SETFAM_1:def 1;

      then

      reconsider I2 = I1 as Subset of L;

      assume I1 <> I;

      per cases ;

        suppose not I1 c= I;

        then

        consider a be object such that

         A1: a in I1 & not a in I;

        a in I2 by A1;

        then

        reconsider a as Element of L;

        consider P be Ideal of L such that

         A2: P is prime & I c= P & not a in P by Cor16, A1;

        P in X by A2;

        then I1 c= P by SETFAM_1: 3;

        hence thesis by A1, A2;

      end;

        suppose not I c= I1;

        then

        consider a be object such that

         A1: a in I & not a in I1;

        consider Y be set such that

         X4: Y in X & not a in Y by SETFAM_1:def 1, A1, k1;

        consider P1 be Ideal of L such that

         X5: Y = P1 & P1 is prime & I c= P1 by X4;

        thus thesis by A1, X4, X5;

      end;

    end;

    begin

    definition

      let L be Lattice;

      :: LATTICEA:def5

      func PrimeFilters L -> Function means

      : Def6: ( dom it ) = the carrier of L & for a be Element of L holds (it . a) = { F where F be Filter of L : F is prime & a in F };

      existence

      proof

        deffunc U( object) = { F where F be Filter of L : F is prime & $1 in F };

        consider f be Function such that

         A1: ( dom f) = the carrier of L and

         A2: for x be object st x in the carrier of L holds (f . x) = U(x) from FUNCT_1:sch 3;

        take f;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let f1,f2 be Function;

        assume that

         A3: ( dom f1) = the carrier of L & for a be Element of L holds (f1 . a) = { F where F be Filter of L : F is prime & a in F } and

         A4: ( dom f2) = the carrier of L & for a be Element of L holds (f2 . a) = { F where F be Filter of L : F is prime & a in F };

        now

          let x be object;

          assume x in the carrier of L;

          then

          reconsider a = x as Element of L;



          thus (f1 . x) = { F where F be Filter of L : F is prime & a in F } by A3

          .= (f2 . x) by A4;

        end;

        hence thesis by A3, A4, FUNCT_1: 2;

      end;

    end

    theorem :: LATTICEA:24



     Th17: for L be Lattice, a be Element of L, x be set holds x in (( PrimeFilters L) . a) iff ex F be Filter of L st F = x & F is prime & a in F

    proof

      let L be Lattice, a be Element of L, x be set;

      thus x in (( PrimeFilters L) . a) implies ex F be Filter of L st F = x & F is prime & a in F

      proof

        assume x in (( PrimeFilters L) . a);

        then x in { F1 where F1 be Filter of L : F1 is prime & a in F1 } by Def6;

        then

        consider F be Filter of L such that

         A2: F = x and

         A3: F is prime and

         A4: a in F;

        take F;

        thus thesis by A2, A3, A4;

      end;

      assume ex F be Filter of L st F = x & F is prime & a in F;

      then x in { F where F be Filter of L : F is prime & a in F };

      hence thesis by Def6;

    end;

    theorem :: LATTICEA:25

    for L be Lattice, a be Element of L, F be Filter of L holds F in (( PrimeFilters L) . a) iff F is prime & a in F

    proof

      let L be Lattice, a be Element of L, F be Filter of L;

      hereby

        assume F in (( PrimeFilters L) . a);

        then ex F0 be Filter of L st F0 = F & F0 is prime & a in F0 by Th17;

        hence F is prime & a in F;

      end;

      thus thesis by Th17;

    end;

    theorem :: LATTICEA:26

    for L be distributive Lattice, a,b be Element of L holds (( PrimeFilters L) . (a "/\" b)) = ((( PrimeFilters L) . a) /\ (( PrimeFilters L) . b))

    proof

      let L be distributive Lattice, a,b be Element of L;



       A1: (( PrimeFilters L) . (a "/\" b)) c= ((( PrimeFilters L) . a) /\ (( PrimeFilters L) . b))

      proof

        let x be object;

        set c = (a "/\" b);

        assume x in (( PrimeFilters L) . c);

        then

        consider F0 be Filter of L such that

         A2: x = F0 and

         A3: F0 is prime and

         A4: c in F0 by Th17;



         A5: a in F0 by A4, FILTER_0: 8;



         A6: b in F0 by A4, FILTER_0: 8;



         A7: F0 in (( PrimeFilters L) . a) by A3, A5, Th17;

        F0 in (( PrimeFilters L) . b) by A3, A6, Th17;

        hence thesis by A2, A7, XBOOLE_0:def 4;

      end;

      ((( PrimeFilters L) . a) /\ (( PrimeFilters L) . b)) c= (( PrimeFilters L) . (a "/\" b))

      proof

        let x be object;

        assume

         A8: x in ((( PrimeFilters L) . a) /\ (( PrimeFilters L) . b));

        then

         A9: x in (( PrimeFilters L) . a) by XBOOLE_0:def 4;



         A10: x in (( PrimeFilters L) . b) by A8, XBOOLE_0:def 4;



         A11: ex F0 be Filter of L st x = F0 & F0 is prime & a in F0 by A9, Th17;

        ex F0 be Filter of L st x = F0 & F0 is prime & b in F0 by A10, Th17;

        then

        consider F0 be Filter of L such that

         A12: x = F0 and

         A13: F0 is prime and

         A14: a in F0 and

         A15: b in F0 by A11;

        (a "/\" b) in F0 by A14, A15, FILTER_0: 8;

        hence thesis by A12, A13, Th17;

      end;

      hence thesis by A1;

    end;

    theorem :: LATTICEA:27

    for L be distributive Lattice, a,b be Element of L holds (( PrimeFilters L) . (a "\/" b)) = ((( PrimeFilters L) . a) \/ (( PrimeFilters L) . b))

    proof

      let L be distributive Lattice, a,b be Element of L;



       A1: (( PrimeFilters L) . (a "\/" b)) c= ((( PrimeFilters L) . a) \/ (( PrimeFilters L) . b))

      proof

        let x be object;

        set c = (a "\/" b);

        assume x in (( PrimeFilters L) . c);

        then

        consider F0 be Filter of L such that

         A2: x = F0 and

         A3: F0 is prime and

         A4: c in F0 by Th17;

        a in F0 or b in F0 by A3, A4, FILTER_0:def 5;

        then F0 in (( PrimeFilters L) . a) or F0 in (( PrimeFilters L) . b) by A3, Th17;

        hence thesis by A2, XBOOLE_0:def 3;

      end;

      ((( PrimeFilters L) . a) \/ (( PrimeFilters L) . b)) c= (( PrimeFilters L) . (a "\/" b))

      proof

        let x be object;

        assume x in ((( PrimeFilters L) . a) \/ (( PrimeFilters L) . b));

        then x in (( PrimeFilters L) . a) or x in (( PrimeFilters L) . b) by XBOOLE_0:def 3;

        then (ex F0 be Filter of L st x = F0 & F0 is prime & a in F0) or ex F0 be Filter of L st x = F0 & F0 is prime & b in F0 by Th17;

        then

        consider F0 be Filter of L such that

         A5: x = F0 and

         A6: F0 is prime and

         A7: a in F0 or b in F0;

        (a "\/" b) in F0 by A6, A7, FILTER_0:def 5;

        hence thesis by A5, A6, Th17;

      end;

      hence thesis by A1;

    end;

    definition

      let L be distributive Lattice;

      :: original: PrimeFilters

      redefine

      func PrimeFilters L -> Function of the carrier of L, ( bool ( PFilters L)) ;

      coherence

      proof

        reconsider f = ( PrimeFilters L) as Function;



         A1: ( dom f) = the carrier of L by Def6;

        ( rng f) c= ( bool ( PFilters L))

        proof

          let y be object;

          reconsider yy = y as set by TARSKI: 1;

          assume y in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) and

           A3: y = (f . x) by FUNCT_1:def 3;

          y = { F where F be Filter of L : F is prime & x in F } by A1, A2, A3, Def6;

          then yy c= ( PFilters L) by A1, A2, Th16;

          hence thesis;

        end;

        then

        reconsider f as Function of the carrier of L, ( bool ( PFilters L)) by A1, FUNCT_2:def 1, RELSET_1: 4;

        for a be Element of L holds (f . a) = { F where F be Filter of L : F is prime & a in F } by Def6;

        hence thesis;

      end;

    end

    definition

      let L be distributive Lattice;

      :: LATTICEA:def6

      func StoneR L -> set equals ( rng ( PrimeFilters L));

      coherence ;

    end

    registration

      let L be distributive Lattice;

      cluster ( StoneR L) -> non empty;

      coherence ;

    end

    theorem :: LATTICEA:28



     Th23: for L be distributive Lattice, x be set holds x in ( StoneR L) iff ex a be Element of L st (( PrimeFilters L) . a) = x

    proof

      let L be distributive Lattice, x be set;

      thus x in ( StoneR L) implies ex a be Element of L st (( PrimeFilters L) . a) = x

      proof

        assume x in ( StoneR L);

        then

        consider y be object such that

         A2: y in ( dom ( PrimeFilters L)) and

         A3: x = (( PrimeFilters L) . y) by FUNCT_1:def 3;

        reconsider a = y as Element of L by A2;

        take a;

        thus thesis by A3;

      end;

      given a be Element of L such that

       A4: x = (( PrimeFilters L) . a);

      a in the carrier of L;

      then a in ( dom ( PrimeFilters L)) by Def6;

      hence thesis by A4, FUNCT_1:def 3;

    end;

    definition

      let L be upper-bounded distributive Lattice;

      :: LATTICEA:def7

      func StoneSpace L -> strict TopSpace means

      : StoneDef: the carrier of it = ( PFilters L) & the topology of it = { ( union A) where A be Subset-Family of ( PFilters L) : A c= ( StoneR L) };

      existence

      proof

        set US = ( PFilters L);

        set STP = { ( union A) where A be Subset-Family of ( PFilters L) : A c= ( StoneR L) };

        STP c= ( bool US)

        proof

          let x be object;

          assume x in STP;

          then ex B be Subset-Family of ( PFilters L) st x = ( union B) & B c= ( StoneR L);

          hence thesis;

        end;

        then

        reconsider STP = { ( union A) where A be Subset-Family of ( PFilters L) : A c= ( StoneR L) } as Subset-Family of US;

         TopStruct (# US, STP #) is strict TopSpace

        proof

          set TS = TopStruct (# US, STP #);



           A1: the carrier of TS in the topology of TS

          proof

            set B = { F where F be Filter of L : F is prime & ( Top L) in F };

            B c= ( PFilters L)

            proof

              let x be object;

              assume x in B;

              then ex F be Filter of L st F = x & F is prime & ( Top L) in F;

              hence thesis;

            end;

            then

             A2: ( bool B) c= ( bool ( PFilters L)) by ZFMISC_1: 67;

             {B} c= ( bool B) by ZFMISC_1: 68;

            then

            reconsider SB = {B} as Subset-Family of ( PFilters L) by A2, XBOOLE_1: 1;

            reconsider SB as Subset-Family of ( PFilters L);

            ( PFilters L) c= B

            proof

              let x be object;

              assume x in ( PFilters L);

              then

              consider F be Filter of L such that

               A4: F = x and

               A5: F is prime;

              ( Top L) in F by FILTER_0: 11;

              hence thesis by A4, A5;

            end;

            then

             A6: ( PFilters L) = ( union SB) by ZFMISC_1: 25;

            (( PrimeFilters L) . ( Top L)) = { F where F be Filter of L : F is prime & ( Top L) in F } by Def6;

            then SB c= ( StoneR L) by ZFMISC_1: 31, Th23;

            hence thesis by A6;

          end;



           A7: for a be Subset-Family of TS st a c= the topology of TS holds ( union a) in the topology of TS

          proof

            let a be Subset-Family of TS;

            assume

             A8: a c= the topology of TS;

            set B = { A where A be Subset of ( StoneR L) : ( union A) in a };

            B c= ( bool ( StoneR L))

            proof

              let x be object;

              assume x in B;

              then ex C be Subset of ( StoneR L) st C = x & ( union C) in a;

              then

              reconsider C = x as Subset of ( StoneR L);

              C c= ( StoneR L);

              hence thesis;

            end;

            then

            reconsider BS = B as Subset-Family of ( StoneR L);



             A9: ( union ( union BS)) = ( union { ( union A) where A be Subset of ( StoneR L) : A in BS }) by EQREL_1: 54;



             A10: a c= { ( union A) where A be Subset of ( StoneR L) : A in BS }

            proof

              let x be object;

              assume

               A11: x in a;

              then x in STP by A8;

              then

              consider C be Subset-Family of ( PFilters L) such that

               A12: x = ( union C) and

               A13: C c= ( StoneR L);

              C in BS by A11, A12, A13;

              hence thesis by A12;

            end;

            { ( union A) where A be Subset of ( StoneR L) : A in BS } c= a

            proof

              let x be object;

              assume x in { ( union A) where A be Subset of ( StoneR L) : A in BS };

              then

              consider C be Subset of ( StoneR L) such that

               A14: ( union C) = x and

               A15: C in BS;

              ex D be Subset of ( StoneR L) st D = C & ( union D) in a by A15;

              hence thesis by A14;

            end;

            then

             A16: a = { ( union A) where A be Subset of ( StoneR L) : A in BS } by A10;

            ( union BS) is Subset-Family of ( PFilters L) by XBOOLE_1: 1;

            hence thesis by A9, A16;

          end;

          for p,q be Subset of TS st p in the topology of TS & q in the topology of TS holds (p /\ q) in the topology of TS

          proof

            let p,q be Subset of TS;

            assume that

             A17: p in the topology of TS and

             A18: q in the topology of TS;

            consider P be Subset-Family of ( PFilters L) such that

             A19: ( union P) = p and

             A20: P c= ( StoneR L) by A17;

            consider Q be Subset-Family of ( PFilters L) such that

             A21: ( union Q) = q and

             A22: Q c= ( StoneR L) by A18;



             A23: (( union P) /\ ( union Q)) = ( union ( INTERSECTION (P,Q))) by SETFAM_1: 28;

            ( INTERSECTION (P,Q)) c= ( bool ( PFilters L))

            proof

              let x be object;

              assume x in ( INTERSECTION (P,Q));

              then

              consider X,Y be set such that

               A24: X in P and

               A25: Y in Q and

               A26: x = (X /\ Y) by SETFAM_1:def 5;



               A27: (X /\ Y) c= (X \/ Y) by XBOOLE_1: 29;

              (X \/ Y) c= ( PFilters L) by A24, A25, XBOOLE_1: 8;

              then (X /\ Y) c= ( PFilters L) by A27;

              hence thesis by A26;

            end;

            then

            reconsider C = ( INTERSECTION (P,Q)) as Subset-Family of ( PFilters L);

            reconsider C as Subset-Family of ( PFilters L);

            C c= ( StoneR L)

            proof

              let x be object;

              assume x in C;

              then

              consider X,Y be set such that

               A28: X in P and

               A29: Y in Q and

               A30: x = (X /\ Y) by SETFAM_1:def 5;

              consider a be Element of L such that

               A31: X = (( PrimeFilters L) . a) by A20, A28, Th23;

              consider b be Element of L such that

               A32: Y = (( PrimeFilters L) . b) by A22, A29, Th23;



               A33: X = { F where F be Filter of L : F is prime & a in F } by A31, Def6;



               A34: Y = { F where F be Filter of L : F is prime & b in F } by A32, Def6;



               A35: (X /\ Y) = { F where F be Filter of L : F is prime & (a "/\" b) in F }

              proof



                 A36: (X /\ Y) c= { F where F be Filter of L : F is prime & (a "/\" b) in F }

                proof

                  let x be object;

                  assume

                   A37: x in (X /\ Y);

                  then

                   A38: x in X by XBOOLE_0:def 4;



                   A39: x in Y by A37, XBOOLE_0:def 4;

                  consider F1 be Filter of L such that

                   A40: x = F1 and

                   A41: F1 is prime and

                   A42: a in F1 by A33, A38;

                  ex F2 be Filter of L st x = F2 & F2 is prime & b in F2 by A34, A39;

                  then (a "/\" b) in F1 by A40, A42, FILTER_0: 8;

                  hence thesis by A40, A41;

                end;

                { F where F be Filter of L : F is prime & (a "/\" b) in F } c= (X /\ Y)

                proof

                  let x be object;

                  assume x in { F where F be Filter of L : F is prime & (a "/\" b) in F };

                  then

                  consider F0 be Filter of L such that

                   A43: x = F0 and

                   A44: F0 is prime and

                   A45: (a "/\" b) in F0;

                  a in F0 by A45, FILTER_0: 8;

                  then

                  consider F be Filter of L such that

                   A46: F = F0 and

                   A47: F is prime and

                   A48: a in F by A44;



                   A49: F in X by A33, A47, A48;

                  b in F0 by A45, FILTER_0: 8;

                  then

                  consider F1 be Filter of L such that

                   A50: F1 = F0 and

                   A51: F1 is prime and

                   A52: b in F1 by A44;

                  F1 in Y by A34, A51, A52;

                  hence thesis by A43, A46, A49, A50, XBOOLE_0:def 4;

                end;

                hence thesis by A36;

              end;

              (( PrimeFilters L) . (a "/\" b)) = { F where F be Filter of L : F is prime & (a "/\" b) in F } by Def6;

              hence thesis by A30, A35, Th23;

            end;

            hence thesis by A19, A21, A23;

          end;

          hence thesis by A1, A7, PRE_TOPC:def 1;

        end;

        then

        reconsider TS = TopStruct (# US, STP #) as strict TopSpace;

        take TS;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let L be non trivial upper-bounded distributive Lattice;

      cluster ( StoneSpace L) -> non empty;

      coherence

      proof

        consider a,b be Element of L such that

         A0: a in ( [#] L) & b in ( [#] L) & a <> b by SUBSET_1: 45;

        consider F be Filter of L such that

         A1: F in ( F_primeSet L) by OPENLATT: 21, A0;

        ( F_primeSet L) c< ( PFilters L) by PrimFil;

        hence thesis by StoneDef, A1;

      end;

    end

    begin

    definition

      let L be Lattice;

      let a be Element of L;

      :: LATTICEA:def8

      func PseudoComplements a -> Subset of L equals { x where x be Element of L : (a "/\" x) = ( Bottom L) };

      coherence

      proof

        set I = { x where x be Element of L : (a "/\" x) = ( Bottom L) };

        I c= the carrier of L

        proof

          let g be object;

          assume g in I;

          then

          consider x1 be Element of L such that

           C1: x1 = g & (a "/\" x1) = ( Bottom L);

          thus thesis by C1;

        end;

        hence thesis;

      end;

      :: LATTICEA:def9

      func PseudoCocomplements a -> Subset of L equals { x where x be Element of L : (a "\/" x) = ( Top L) };

      coherence

      proof

        set I = { x where x be Element of L : (a "\/" x) = ( Top L) };

        I c= the carrier of L

        proof

          let g be object;

          assume g in I;

          then

          consider x1 be Element of L such that

           C1: x1 = g & (a "\/" x1) = ( Top L);

          thus thesis by C1;

        end;

        hence thesis;

      end;

    end



     LemDistr: for L be distributive Lattice, a,x1,x2 be Element of L holds (a "\/" (x1 "/\" x2)) = ((a "\/" x1) "/\" (a "\/" x2))

    proof

      let L be distributive Lattice, a,x1,x2 be Element of L;

      for a,b,c be Element of L holds (a "/\" (b "\/" c)) = ((a "/\" b) "\/" (a "/\" c)) by LATTICES:def 11;

      hence thesis by LATTICES: 3;

    end;

    registration

      let L be distributive bounded Lattice;

      let a be Element of L;

      cluster ( PseudoComplements a) -> initial non empty join-closed;

      coherence

      proof

        set I0 = ( PseudoComplements a);



         CC: for p,q be Element of L st p [= q & q in I0 holds p in I0

        proof

          let p,q be Element of L;

          assume

           C0: p [= q & q in I0;

          then

          consider x1 be Element of L such that

           C1: x1 = q & (a "/\" x1) = ( Bottom L);



           C2: ( Bottom L) [= (a "/\" p);

          (a "/\" p) [= (a "/\" q) by C0, LATTICES: 9;

          then (a "/\" p) = ( Bottom L) by C2, LATTICES: 8, C1;

          hence thesis;

        end;



         C2: for p,q be Element of L st p in I0 & q in I0 holds (p "\/" q) in I0

        proof

          let p,q be Element of L;

          assume

           d0: p in I0 & q in I0;

          then

          consider x1 be Element of L such that

           d1: x1 = p & (a "/\" x1) = ( Bottom L);

          consider x2 be Element of L such that

           d2: x2 = q & (a "/\" x2) = ( Bottom L) by d0;

          (a "/\" (x1 "\/" x2)) = ((a "/\" x1) "\/" (a "/\" x2)) by LATTICES:def 11

          .= ( Bottom L) by d1, d2;

          hence thesis by d1, d2;

        end;

        (a "/\" ( Bottom L)) = ( Bottom L);

        then ( Bottom L) in I0;

        hence thesis by CC, C2;

      end;

      cluster ( PseudoCocomplements a) -> final non empty meet-closed;

      coherence

      proof

        set I0 = ( PseudoCocomplements a);



         CC: for p,q be Element of L st p [= q & p in I0 holds q in I0

        proof

          let p,q be Element of L;

          assume

           C0: p [= q & p in I0;

          then

          consider x1 be Element of L such that

           C1: x1 = p & (a "\/" x1) = ( Top L);

          (a "\/" p) [= (a "\/" q) by C0, FILTER_0: 1;

          hence thesis by C1;

        end;



         C2: for p,q be Element of L st p in I0 & q in I0 holds (p "/\" q) in I0

        proof

          let p,q be Element of L;

          assume

           d0: p in I0 & q in I0;

          then

          consider x1 be Element of L such that

           d1: x1 = p & (a "\/" x1) = ( Top L);

          consider x2 be Element of L such that

           d2: x2 = q & (a "\/" x2) = ( Top L) by d0;

          (a "\/" (x1 "/\" x2)) = ((a "\/" x1) "/\" (a "\/" x2)) by LemDistr

          .= ( Top L) by d1, d2;

          hence thesis by d1, d2;

        end;

        (a "\/" ( Top L)) = ( Top L);

        then ( Top L) in I0;

        hence thesis by CC, C2;

      end;

    end

    theorem :: LATTICEA:29

    for L be Lattice, a,b be Element of L holds b in ( PseudoComplements a) iff (b "/\" a) = ( Bottom L)

    proof

      let L be Lattice, a,b be Element of L;

      hereby

        assume b in ( PseudoComplements a);

        then

        consider x be Element of L such that

         A1: b = x & (a "/\" x) = ( Bottom L);

        thus (b "/\" a) = ( Bottom L) by A1;

      end;

      assume (b "/\" a) = ( Bottom L);

      hence thesis;

    end;

    theorem :: LATTICEA:30

    for L be Lattice, a,b be Element of L holds b in ( PseudoCocomplements a) iff (b "\/" a) = ( Top L)

    proof

      let L be Lattice, a,b be Element of L;

      hereby

        assume b in ( PseudoCocomplements a);

        then

        consider x be Element of L such that

         A1: b = x & (a "\/" x) = ( Top L);

        thus (b "\/" a) = ( Top L) by A1;

      end;

      assume (b "\/" a) = ( Top L);

      hence thesis;

    end;

    theorem :: LATTICEA:31

    for L be bounded Lattice, a be Element of L holds ( Bottom L) in ( PseudoComplements a)

    proof

      let L be bounded Lattice, a be Element of L;

      (a "/\" ( Bottom L)) = ( Bottom L);

      hence thesis;

    end;

    theorem :: LATTICEA:32

    for L be bounded Lattice, a be Element of L holds ( Top L) in ( PseudoCocomplements a)

    proof

      let L be bounded Lattice, a be Element of L;

      (a "\/" ( Top L)) = ( Top L);

      hence thesis;

    end;

    begin

    definition

      let L be Lattice;

      :: LATTICEA:def10

      func Spectrum L -> Subset-Family of L equals { I where I be Ideal of L : I is prime proper };

      coherence

      proof

        set US = { F where F be Ideal of L : F is prime proper };

        US c= ( bool the carrier of L)

        proof

          let x be object;

          assume x in US;

          then ex UF be Ideal of L st UF = x & UF is prime proper;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    ::$Notion-Name

    theorem :: LATTICEA:33

    for L be distributive bounded Lattice holds L is Boolean iff for I be Ideal of L st I is proper prime holds I is maximal

    proof

      let L be distributive bounded Lattice;

      thus L is Boolean implies for I be Ideal of L st I is proper prime holds I is maximal

      proof

        assume

         YY: L is Boolean;

        let I be Ideal of L;

        assume

         Y0: I is proper prime;

        for G be Ideal of L st G is proper & I c= G holds I = G

        proof

          let G be Ideal of L;

          assume

           y1: G is proper & I c= 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 thesis by FILTER_2:def 8, y1, y3;

        end;

        hence I is maximal by Y0;

      end;

      assume

       A1: for I be Ideal of L st I is proper prime holds I is maximal;

      assume not L is Boolean;

      then not L is complemented;

      then

      consider a be Element of L such that

       A2: not ex b be Element of L st b is_a_complement_of a;

      set I0 = ( PseudoComplements a);

      reconsider I0 as Ideal of L;

      (a "/\" ( Bottom L)) = ( Bottom L);

      then

       C2: ( Bottom L) in I0;

      set I1 = { x where x be Element of L : ex y be Element of L st y in I0 & x [= (a "\/" y) };

      I1 c= the carrier of L

      proof

        let g be object;

        assume g in I1;

        then

        consider x1 be Element of L such that

         C1: x1 = g & ex y be Element of L st y in I0 & x1 [= (a "\/" y);

        thus thesis by C1;

      end;

      then

      reconsider I1 as Subset of L;

      for p,q be Element of L st p [= q & q in I1 holds p in I1

      proof

        let p,q be Element of L;

        assume

         C0: p [= q & q in I1;

        then

        consider x1 be Element of L such that

         C1: x1 = q & ex y be Element of L st y in I0 & x1 [= (a "\/" y);

        consider y be Element of L such that

         CC: y in I0 & x1 [= (a "\/" y) by C1;

        p [= (a "\/" y) by C1, C0, LATTICES: 7, CC;

        hence thesis by CC;

      end;

      then

       C1: I1 is initial;

      for p,q be Element of L st p in I1 & q in I1 holds (p "\/" q) in I1

      proof

        let p,q be Element of L;

        assume

         d0: p in I1 & q in I1;

        then

        consider x1 be Element of L such that

         d1: x1 = p & ex y be Element of L st y in I0 & x1 [= (a "\/" y);

        consider y1 be Element of L such that

         e1: y1 in I0 & x1 [= (a "\/" y1) by d1;

        consider x2 be Element of L such that

         d2: x2 = q & ex y be Element of L st y in I0 & x2 [= (a "\/" y) by d0;

        consider y2 be 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 thesis by HH, d1, d2, FF;

      end;

      then

       CC: I1 is join-closed;

      a [= (a "\/" ( Bottom L));

      then

       ZZ: a in I1 by C2;

      then

      reconsider I1 as Ideal of L by C1, CC;



       q1: I0 c= I1

      proof

        let t be object;

        assume

         C0: t in I0;

        then

        consider x1 be Element of L such that

         C1: x1 = t & (a "/\" x1) = ( Bottom L);

        x1 [= (a "\/" x1) by LATTICES: 5;

        hence thesis by C1, C0;

      end;



       J1: not ( Top L) in I1

      proof

        assume ( Top L) in I1;

        then

        consider x1 be Element of L such that

         D1: x1 = ( Top L) & ex y be Element of L st y in I0 & x1 [= (a "\/" y);

        consider y be Element of L such that

         D2: y in I0 & ( Top L) [= (a "\/" y) by D1;

        consider x2 be Element of L such that

         C1: x2 = y & (a "/\" x2) = ( Bottom L) by D2;

        y is_a_complement_of a by C1, D2;

        hence thesis by A2;

      end;

      set FF = <.( Top L).);

      FF = [#( Top L), ( Top L)#] by FILTER_2: 65;

      then

       J2: FF = {( Top L)} by FILTER_2: 64;

      then FF misses I1 by J1, ZFMISC_1: 50;

      then

      consider J0 be Ideal of L such that

       B1: J0 is prime & I1 c= J0 & J0 misses FF by Th15;



       S4: J0 <> the carrier of L by B1, ZFMISC_1: 48, J2;

      set T = the carrier of L;

      reconsider D = (T \ J0) as non empty Subset of L by S4, XBOOLE_1: 37;

      for p,q be Element of L st p [= q & p in D holds q in D

      proof

        let p,q be Element of L;

        assume

         k0: p [= q & p in D;

        then p in T & not p in J0 by XBOOLE_0:def 5;

        then not q in J0 by k0, FILTER_2: 21;

        hence thesis by XBOOLE_0:def 5;

      end;

      then

       j1: D is final;

      for p,q be Element of L st p in D & q in D holds (p "/\" q) in D

      proof

        let p,q be Element of L;

        assume p in D & q in D;

        then p in T & not p in J0 & q in T & not q in J0 by XBOOLE_0:def 5;

        then not (p "/\" q) in J0 by FILTER_2:def 10, B1;

        hence thesis by XBOOLE_0:def 5;

      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 T c= J0 by B1, ZFMISC_1: 48, J2;

      then

       G2: (T \ 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;

        then

        consider h be object such that

         H1: h in F & h in I0 by XBOOLE_0: 3;

        consider x1 be Element of L such that

         C1: x1 = h & (a "/\" x1) = ( Bottom L) by H1;

        consider b be object such that

         n1: b in (T \ J0) by XBOOLE_0:def 1, G2;

        reconsider b as Element of L by n1;

        consider bb be 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 thesis by W1, B1, q1;

      end;

      then

      consider J1 be 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;

        assume

         f3: t in J1;

        then not t in D by mm, B2, XBOOLE_0: 3;

        hence thesis by f3, XBOOLE_0:def 5;

      end;

      then not J1 is maximal by S2, S3;

      hence thesis by B2, A1, S1;

    end;

    registration

      let L be non trivial distributive bounded Lattice;

      cluster ( Spectrum L) -> non empty;

      coherence

      proof

        set p = ( Bottom L);

        ( Bottom L) <> ( Top L) by TopBot;

        then

        consider I be Ideal of L such that

         A0: p in I & I is max-ideal by FILTER_2: 35;



         a2: I <> the carrier of L by FILTER_2:def 8, A0;

        for G be Ideal of L st G is proper & I c= G holds I = G

        proof

          let G be Ideal of L;

          assume

           B1: G is proper & I c= G;

          then G <> the carrier of L by SUBSET_1:def 6;

          hence thesis by FILTER_2:def 8, A0, B1;

        end;

        then I is maximal by a2, SUBSET_1:def 6;

        then I in ( Spectrum L);

        hence thesis;

      end;

    end

    ::$Notion-Name

    theorem :: LATTICEA:34



     NachSpec: for L be distributive bounded Lattice holds L is Boolean iff ( Spectrum L) is unordered

    proof

      let L be distributive bounded Lattice;

      thus L is Boolean implies ( Spectrum L) is unordered

      proof

        assume L is Boolean;

        then

        reconsider LL = L as Boolean Lattice;

        assume not ( Spectrum L) is unordered;

        then

        consider P,Q be set such that

         F1: P in ( Spectrum L) & Q in ( Spectrum L) & P <> Q & (P,Q) are_c=-comparable ;

        consider P1 be Ideal of L such that

         B1: P1 = P & P1 is prime proper by F1;

        consider Q1 be Ideal of LL such that

         b1: Q1 = Q & Q1 is prime proper by F1;

         A2:

        now

          assume

           f1: P c= Q;

          then P c< Q by F1;

          then (Q \ P) <> {} by XBOOLE_1: 105;

          then

          consider a be 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 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;

        end;

        now

          assume

           f1: Q c= P;

          then Q c< P by F1;

          then (P \ Q) <> {} by XBOOLE_1: 105;

          then

          consider a be 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 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;

        end;

        hence thesis by A2, F1;

      end;

      assume

       d1: ( Spectrum L) is unordered;

      assume not L is Boolean;

      then not L is complemented;

      then

      consider a be Element of L such that

       C2: not ex b be Element of L st b is_a_complement_of a;

      set D = ( PseudoCocomplements a);

      reconsider D as Filter of L;

      set D1 = <.(D \/ <.a.)).);



       II: D1 = { r where r be Element of L : ex d,q be Element of L st (d "/\" q) [= r & d in D & q in <.a.) } by FILTER_0: 35;



       AB: D1 c= { x where x be Element of L : ex d be Element of L st d in D & (a "/\" d) [= x }

      proof

        let t be object;

        assume t in D1;

        then

        consider r be Element of L such that

         I1: r = t & ex d,q be Element of L st (d "/\" q) [= r & d in D & q in <.a.) by II;

        consider d,q be Element of L such that

         I2: (d "/\" q) [= r & d in D & q in <.a.) by I1;

        a [= q by I2, FILTER_0: 15;

        then (d "/\" a) [= (d "/\" q) by FILTER_0: 5;

        then (d "/\" a) [= r by I2, LATTICES: 7;

        hence thesis by I1, I2;

      end;

      { x where x be Element of L : ex d be Element of L st d in D & (a "/\" d) [= x } c= D1

      proof

        let t be object;

        assume t in { x where x be Element of L : ex d be Element of L st d in D & (a "/\" d) [= x };

        then

        consider x1 be Element of L such that

         a1: x1 = t & ex d be Element of L st d in D & (a "/\" d) [= x1;

        consider d be Element of L such that

         a2: d in D & (a "/\" d) [= x1 by a1;

        set q = a;

        (d "/\" q) [= x1 & q in <.a.) by a2;

        hence thesis by a1, II;

      end;

      then

       Z0: D1 = { x where x be Element of L : ex d be 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 D1 by Z0;

      reconsider D1 as Filter of L;



       HJ: not ( Bottom L) in D1

      proof

        assume ( Bottom L) in D1;

        then

        consider y be Element of L such that

         Z1: y = ( Bottom L) & ex d be Element of L st d in D & (a "/\" d) [= y by Z0;

        consider d be Element of L such that

         Z2: d in D & (d "/\" a) [= y by Z1;



         z4: ( Bottom L) [= (d "/\" a);

        consider x be Element of L such that

         Z3: d = x & (a "\/" x) = ( Top L) by Z2;

        d is_a_complement_of a by z4, Z3, Z1, Z2, LATTICES: 8;

        hence thesis by C2;

      end;

      reconsider I0 = {( Bottom L)} as Ideal of L by FILTER_2: 25;

      consider P be 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 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

      proof

        assume

         f2: ( Top L) in Pa;

         (.(P \/ (.a.>).> = { r where r be Element of L : ex p,q be Element of L st r [= (p "\/" q) & p in P & q in (.a.> } by FILTER_2: 49;

        then

        consider r be Element of L such that

         F3: r = ( Top L) & ex p,q be Element of L st r [= (p "\/" q) & p in P & q in (.a.> by f2;

        consider p,q be Element of L such that

         F4: ( Top L) [= (p "\/" q) & p in P & q in (.a.> by F3;



         F5: ( Top L) [= (p "\/" a) by FILTER_0: 1, F4, FILTER_2: 28;

        p in { x where x be Element of L : (a "\/" x) = ( Top L) } by F5;

        hence thesis by hh, XBOOLE_0: 3, F4, W0;

      end;

      then

      consider QQ be 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 thesis by d1, W2, W3;

    end;

    registration

      let L be Boolean Lattice;

      cluster ( Spectrum L) -> unordered;

      coherence by NachSpec;

    end