openlatt.miz

    begin

    registration

      cluster Heyting -> implicative for 0_Lattice;

      coherence ;

      cluster implicative -> upper-bounded for Lattice;

      coherence ;

    end

    reserve T for TopSpace;

    reserve A,B for Subset of T;

    theorem :: OPENLATT:1



     Th1: (A /\ ( Int ((A ` ) \/ B))) c= B

    proof



       A1: A misses (A ` ) by XBOOLE_1: 79;

      (A /\ ((A ` ) \/ B)) = ((A /\ (A ` )) \/ (A /\ B)) by XBOOLE_1: 23

      .= ( {} \/ (A /\ B)) by A1

      .= (A /\ B);

      then

       A2: (A /\ ((A ` ) \/ B)) c= B by XBOOLE_1: 17;

      (A /\ ( Int ((A ` ) \/ B))) c= (A /\ ((A ` ) \/ B)) by TOPS_1: 16, XBOOLE_1: 26;

      hence thesis by A2;

    end;

    theorem :: OPENLATT:2



     Th2: for C be Subset of T st C is open & (A /\ C) c= B holds C c= ( Int ((A ` ) \/ B))

    proof

      let C be Subset of T;

      assume that

       A1: C is open and

       A2: (A /\ C) c= B;



       A3: C c= (C \/ (A ` )) by XBOOLE_1: 7;

      ((A /\ C) \/ (A ` )) = ((A \/ (A ` )) /\ (C \/ (A ` ))) by XBOOLE_1: 24

      .= (( [#] T) /\ (C \/ (A ` ))) by PRE_TOPC: 2

      .= (C \/ (A ` )) by XBOOLE_1: 28;

      then (C \/ (A ` )) c= (B \/ (A ` )) by A2, XBOOLE_1: 9;

      then C c= (B \/ (A ` )) by A3;

      then ( Int C) c= ( Int ((A ` ) \/ B)) by TOPS_1: 19;

      hence thesis by A1, TOPS_1: 23;

    end;

    definition

      let T be TopStruct;

      :: OPENLATT:def1

      func Topology_of T -> Subset-Family of T equals the topology of T;

      coherence ;

    end

    registration

      let T;

      cluster ( Topology_of T) -> non empty;

      coherence ;

    end

    definition

      let T be non empty TopSpace, P,Q be Element of ( Topology_of T);

      :: original: \/

      redefine

      func P \/ Q -> Element of ( Topology_of T) ;

      coherence

      proof

        reconsider A = P, B = Q as Subset of T;



         A1: B is open;

        A is open;

        then (P \/ Q) is open by A1;

        hence thesis;

      end;

      :: original: /\

      redefine

      func P /\ Q -> Element of ( Topology_of T) ;

      coherence

      proof

        reconsider A = P, B = Q as Subset of T;



         A2: B is open;

        A is open;

        then (P /\ Q) is open by A2;

        hence thesis;

      end;

    end

    reserve T for non empty TopSpace;

    reserve P,Q for Element of ( Topology_of T);

    definition

      let T;

      :: OPENLATT:def2

      func Top_Union T -> BinOp of ( Topology_of T) means

      : Def2: (it . (P,Q)) = (P \/ Q);

      existence

      proof

        deffunc F( Element of ( Topology_of T), Element of ( Topology_of T)) = ($1 \/ $2);

        thus ex F be BinOp of ( Topology_of T) st for P,Q be Element of ( Topology_of T) holds (F . (P,Q)) = F(P,Q) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        set A = ( Topology_of T);

        deffunc O( Element of A, Element of A) = ($1 \/ $2);

        thus for o1,o2 be BinOp of A st (for a,b be Element of A holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of A holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

      :: OPENLATT:def3

      func Top_Meet T -> BinOp of ( Topology_of T) means

      : Def3: (it . (P,Q)) = (P /\ Q);

      existence

      proof

        deffunc F( Element of ( Topology_of T), Element of ( Topology_of T)) = ($1 /\ $2);

        thus ex F be BinOp of ( Topology_of T) st for P,Q be Element of ( Topology_of T) holds (F . (P,Q)) = F(P,Q) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        set A = ( Topology_of T);

        deffunc O( Element of A, Element of A) = ($1 /\ $2);

        thus for o1,o2 be BinOp of A st (for a,b be Element of A holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of A holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    theorem :: OPENLATT:3



     Th3: for T be non empty TopSpace holds LattStr (# ( Topology_of T), ( Top_Union T), ( Top_Meet T) #) is Lattice

    proof

      let T;

      set L = LattStr (# ( Topology_of T), ( Top_Union T), ( Top_Meet T) #);

       A1:

      now

        let p,q be Element of L;



        thus (p "\/" q) = (q \/ p) by Def2

        .= (q "\/" p) by Def2;

      end;

       A2:

      now

        let p,q be Element of L;



        thus ((p "/\" q) "\/" q) = ((p "/\" q) \/ q) by Def2

        .= ((p /\ q) \/ q) by Def3

        .= q by XBOOLE_1: 22;

      end;

       A3:

      now

        let p,q be Element of L;



        thus (p "/\" (p "\/" q)) = (p /\ (p "\/" q)) by Def3

        .= (p /\ (p \/ q)) by Def2

        .= p by XBOOLE_1: 21;

      end;

       A4:

      now

        let p,q,r be Element of L;



        thus (p "/\" (q "/\" r)) = (p /\ (q "/\" r)) by Def3

        .= (p /\ (q /\ r)) by Def3

        .= ((p /\ q) /\ r) by XBOOLE_1: 16

        .= ((p "/\" q) /\ r) by Def3

        .= ((p "/\" q) "/\" r) by Def3;

      end;

       A5:

      now

        let p,q be Element of L;



        thus (p "/\" q) = (q /\ p) by Def3

        .= (q "/\" p) by Def3;

      end;

      now

        let p,q,r be Element of L;



        thus (p "\/" (q "\/" r)) = (p \/ (q "\/" r)) by Def2

        .= (p \/ (q \/ r)) by Def2

        .= ((p \/ q) \/ r) by XBOOLE_1: 4

        .= ((p "\/" q) \/ r) by Def2

        .= ((p "\/" q) "\/" r) by Def2;

      end;

      then L is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A2, A5, A4, A3;

      hence thesis;

    end;

    definition

      let T;

      :: OPENLATT:def4

      func Open_setLatt (T) -> Lattice equals LattStr (# ( Topology_of T), ( Top_Union T), ( Top_Meet T) #);

      coherence by Th3;

    end

    theorem :: OPENLATT:4

    the carrier of ( Open_setLatt T) = ( Topology_of T);

    reserve p,q for Element of ( Open_setLatt T);

    theorem :: OPENLATT:5

    (p "\/" q) = (p \/ q) & (p "/\" q) = (p /\ q) by Def2, Def3;

    theorem :: OPENLATT:6



     Th6: p [= q iff p c= q

    proof

      (p "\/" q) = (p \/ q) by Def2;

      hence thesis by XBOOLE_1: 7, XBOOLE_1: 12;

    end;

    theorem :: OPENLATT:7



     Th7: for p9,q9 be Element of ( Topology_of T) st p = p9 & q = q9 holds p [= q iff p9 c= q9

    proof

      let p9,q9 be Element of ( Topology_of T) such that

       A1: p = p9 and

       A2: q = q9;

      hereby

        assume

         A3: p [= q;

        (p9 \/ q9) = (p "\/" q) by A1, A2, Def2

        .= q9 by A2, A3;

        hence p9 c= q9 by XBOOLE_1: 7;

      end;

      assume

       A4: p9 c= q9;

      (p "\/" q) = (p9 \/ q9) by A1, A2, Def2

      .= q by A2, A4, XBOOLE_1: 12;

      hence thesis;

    end;

    registration

      let T;

      cluster ( Open_setLatt T) -> implicative;

      coherence

      proof

        set OL = ( Open_setLatt T);

        let p,q be Element of OL;

        reconsider p9 = p, q9 = q as Element of ( Topology_of T);

        reconsider r9 = ( Int ((p9 ` ) \/ q9)) as Element of ( Topology_of T) by PRE_TOPC:def 2;

        reconsider r = r9 as Element of OL;

        take r;



         A1: (p "/\" r) = (p9 /\ r9) by Def3;

        (p9 /\ r) c= q9 by Th1;

        hence (p "/\" r) [= q by A1, Th7;

        let r1 be Element of OL;

        reconsider r2 = r1 as Element of ( Topology_of T);

        reconsider r19 = r2 as Subset of T;



         A2: r19 is open;

        assume

         A3: (p "/\" r1) [= q;

        (p "/\" r1) = (p9 /\ r19) by Def3;

        then (p9 /\ r2) c= q9 by A3, Th7;

        then r19 c= r9 by A2, Th2;

        hence r1 [= r by Th7;

      end;

    end

    theorem :: OPENLATT:8



     Th8: ( Open_setLatt T) is lower-bounded & ( Bottom ( Open_setLatt T)) = {}

    proof

      set OL = ( Open_setLatt T);

      reconsider r = {} as Element of OL by PRE_TOPC: 1;

       A1:

      now

        let p;



        thus (r "/\" p) = (r /\ p) by Def3

        .= r;

        hence (p "/\" r) = r;

      end;

      thus OL is lower-bounded by A1;

      hence thesis by A1, LATTICES:def 16;

    end;

    registration

      let T;

      cluster ( Open_setLatt T) -> Heyting;

      coherence

      proof

        reconsider OL = ( Open_setLatt T) as 0_Lattice by Th8;

        OL is I_Lattice;

        hence thesis;

      end;

    end

    theorem :: OPENLATT:9



     Th9: ( Top ( Open_setLatt T)) = the carrier of T

    proof

      set OL = ( Open_setLatt T);

      reconsider B = the carrier of T as Element of OL by PRE_TOPC:def 1;

      now

        let p be Element of OL;

        reconsider p9 = p as Element of ( Topology_of T);



        thus (B "\/" p) = (the carrier of T \/ p9) by Def2

        .= B by XBOOLE_1: 12;

        hence (p "\/" B) = B;

      end;

      hence thesis by LATTICES:def 17;

    end;

    reserve L for D_Lattice;

    reserve F for Filter of L;

    reserve a,b for Element of L;

    reserve x,X,X1,X2,Y,Z for set;

    definition

      let L;

      :: OPENLATT:def5

      func F_primeSet (L) -> set equals { F : F <> the carrier of L & F is prime };

      coherence ;

    end

    theorem :: OPENLATT:10



     Th10: F in ( F_primeSet L) iff F <> the carrier of L & F is prime

    proof

      F in ( F_primeSet L) iff ex F0 be Filter of L st F0 = F & F0 <> the carrier of L & F0 is prime;

      hence thesis;

    end;

    definition

      let L;

      :: OPENLATT:def6

      func StoneH (L) -> Function means

      : Def6: ( dom it ) = the carrier of L & (it . a) = { F : F in ( F_primeSet L) & a in F };

      existence

      proof

        deffunc F( object) = { F : F in ( F_primeSet L) & $1 in F };

        consider f be Function such that

         A1: ( dom f) = the carrier of L & for x be object st x in the carrier of L holds (f . x) = F(x) from FUNCT_1:sch 3;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be Function;

        assume that

         A2: ( dom f1) = the carrier of L & (f1 . a) = { F : F in ( F_primeSet L) & a in F } and

         A3: ( dom f2) = the carrier of L & (f2 . a) = { F : F in ( F_primeSet L) & 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 : F in ( F_primeSet L) & a in F } by A2

          .= (f2 . x) by A3;

        end;

        hence thesis by A2, A3;

      end;

    end

    theorem :: OPENLATT:11



     Th11: F in (( StoneH L) . a) iff F in ( F_primeSet L) & a in F

    proof

      (( StoneH L) . a) = { F0 where F0 be Filter of L : F0 in ( F_primeSet L) & a in F0 } by Def6;

      then F in (( StoneH L) . a) iff ex F0 be Filter of L st F = F0 & F0 in ( F_primeSet L) & a in F0;

      hence thesis;

    end;

    theorem :: OPENLATT:12



     Th12: x in (( StoneH L) . a) iff ex F st F = x & F <> the carrier of L & F is prime & a in F

    proof



       A1: (( StoneH L) . a) = { F : F in ( F_primeSet L) & a in F } by Def6;

      hereby

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

        then

        consider F such that

         A2: x = F and

         A3: F in ( F_primeSet L) and

         A4: a in F by A1;



         A5: F is prime by A3, Th10;

        F <> the carrier of L by A3, Th10;

        hence ex F st F = x & F <> the carrier of L & F is prime & a in F by A2, A4, A5;

      end;

      given F such that

       A6: F = x and

       A7: F <> the carrier of L and

       A8: F is prime and

       A9: a in F;

      F in ( F_primeSet L) by A7, A8;

      hence thesis by A1, A6, A9;

    end;

    definition

      let L;

      :: OPENLATT:def7

      func StoneS (L) -> set equals ( rng ( StoneH L));

      coherence ;

    end

    registration

      let L;

      cluster ( StoneS L) -> non empty;

      coherence

      proof

        ( dom ( StoneH L)) = the carrier of L by Def6;

        hence thesis by RELAT_1: 42;

      end;

    end

    theorem :: OPENLATT:13



     Th13: x in ( StoneS L) iff ex a st x = (( StoneH L) . a)

    proof

      hereby

        assume x in ( StoneS L);

        then

        consider y be object such that

         A1: y in ( dom ( StoneH L)) and

         A2: x = (( StoneH L) . y) by FUNCT_1:def 3;

        reconsider y as Element of L by A1, Def6;

        take y;

        thus x = (( StoneH L) . y) by A2;

      end;

      given b such that

       A3: x = (( StoneH L) . b);

      b in the carrier of L;

      then b in ( dom ( StoneH L)) by Def6;

      hence thesis by A3, FUNCT_1:def 3;

    end;

    theorem :: OPENLATT:14



     Th14: (( StoneH L) . (a "\/" b)) = ((( StoneH L) . a) \/ (( StoneH L) . b))

    proof

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

      hereby

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

        let x be object;

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

        then

        consider F such that

         A1: x = F and

         A2: F <> the carrier of L and

         A3: F is prime and

         A4: c in F by Th12;

        a in F or b in F by A3, A4;

        then F in (( StoneH L) . a) or F in (( StoneH L) . b) by A2, A3, Th12;

        hence x in ((( StoneH L) . a) \/ (( StoneH L) . b)) by A1, XBOOLE_0:def 3;

      end;

      let x be object;

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

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

      then (ex F st x = F & F <> the carrier of L & F is prime & a in F) or ex F st x = F & F <> the carrier of L & F is prime & b in F by Th12;

      then

      consider F such that

       A5: x = F and

       A6: F <> the carrier of L and

       A7: F is prime and

       A8: a in F or b in F;

      c in F by A7, A8;

      hence thesis by A5, A6, A7, Th12;

    end;

    theorem :: OPENLATT:15



     Th15: (( StoneH L) . (a "/\" b)) = ((( StoneH L) . a) /\ (( StoneH L) . b))

    proof

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

      hereby

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

        let x be object;

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

        then

        consider F such that

         A1: x = F and

         A2: F <> the carrier of L and

         A3: F is prime and

         A4: c in F by Th12;

        b in F by A4, FILTER_0: 8;

        then

         A5: F in (( StoneH L) . b) by A2, A3, Th12;

        a in F by A4, FILTER_0: 8;

        then F in (( StoneH L) . a) by A2, A3, Th12;

        hence x in ((( StoneH L) . a) /\ (( StoneH L) . b)) by A1, A5, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A6: x in ((( StoneH L) . a) /\ (( StoneH L) . b));

      then x in (( StoneH L) . b) by XBOOLE_0:def 4;

      then

       A7: ex F st x = F & F <> the carrier of L & F is prime & b in F by Th12;

      x in (( StoneH L) . a) by A6, XBOOLE_0:def 4;

      then ex F st x = F & F <> the carrier of L & F is prime & a in F by Th12;

      then

      consider F such that

       A8: x = F and

       A9: F <> the carrier of L and

       A10: F is prime and

       A11: a in F and

       A12: b in F by A7;

      c in F by A11, A12, FILTER_0: 8;

      hence thesis by A8, A9, A10, Th12;

    end;

    definition

      let L, a;

      :: OPENLATT:def8

      func SF_have a -> Subset-Family of L equals { F : a in F };

      coherence

      proof

        set A = { F : a in F };

        A c= ( bool the carrier of L)

        proof

          let x be object;

          assume x in A;

          then ex F st x = F & a in F;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let L;

      let a;

      cluster ( SF_have a) -> non empty;

      coherence

      proof

        a in <.a.);

        then <.a.) in { F : a in F };

        hence thesis;

      end;

    end

    theorem :: OPENLATT:16



     Th16: x in ( SF_have a) iff x is Filter of L & a in x

    proof

      x in ( SF_have a) iff ex F st F = x & a in F;

      hence thesis;

    end;



     Lm1: F in (( SF_have b) \ ( SF_have a)) iff b in F & not a in F

    proof

      F in (( SF_have b) \ ( SF_have a)) iff F in ( SF_have b) & not F in ( SF_have a) by XBOOLE_0:def 5;

      hence thesis by Th16;

    end;

    theorem :: OPENLATT:17



     Th17: x in (( SF_have b) \ ( SF_have a)) implies x is Filter of L & b in x & not a in x

    proof

      assume

       A1: x in (( SF_have b) \ ( SF_have a));

      then

       A2: not x in ( SF_have a) by XBOOLE_0:def 5;



       A3: x in ( SF_have b) by A1, XBOOLE_0:def 5;

      then x is Filter of L by Th16;

      hence thesis by A3, A2, Th16;

    end;

    theorem :: OPENLATT:18



     Th18: for Z st Z <> {} & Z c= (( SF_have b) \ ( SF_have a)) & Z is c=-linear holds ex Y st Y in (( SF_have b) \ ( SF_have a)) & for X1 st X1 in Z holds X1 c= Y

    proof

      let Z;

      assume that

       A1: Z <> {} and

       A2: Z c= (( SF_have b) \ ( SF_have a)) and

       A3: Z is c=-linear;

      reconsider Z as Subset-Family of L by A2, XBOOLE_1: 1;

      take Y = ( union Z);

      Y in (( SF_have b) \ ( SF_have a))

      proof

        set X = the Element of Z;



         A4: not a in Y

        proof

          assume a in Y;

          then ex X st a in X & X in Z by TARSKI:def 4;

          hence contradiction by A2, Th17;

        end;

        X in (( SF_have b) \ ( SF_have a)) by A1, A2;

        then

         A5: b in X by Th17;

        then

         A6: b in Y by A1, TARSKI:def 4;

        reconsider Y as non empty Subset of L by A1, A5, TARSKI:def 4;

        now

          let p,q be Element of L;

          thus p in Y & q in Y implies (p "/\" q) in Y

          proof

            assume p in Y;

            then

            consider X1 such that

             A7: p in X1 and

             A8: X1 in Z by TARSKI:def 4;



             A9: X1 is Filter of L by A2, A8, Th17;

            assume q in Y;

            then

            consider X2 such that

             A10: q in X2 and

             A11: X2 in Z by TARSKI:def 4;

            (X1,X2) are_c=-comparable by A3, A8, A11, ORDINAL1:def 8;

            then

             A12: X1 c= X2 or X2 c= X1;

            X2 is Filter of L by A2, A11, Th17;

            then (p "/\" q) in X1 or (p "/\" q) in X2 by A7, A10, A9, A12, FILTER_0: 8;

            hence thesis by A8, A11, TARSKI:def 4;

          end;

          assume (p "/\" q) in Y;

          then

          consider X1 such that

           A13: (p "/\" q) in X1 and

           A14: X1 in Z by TARSKI:def 4;



           A15: X1 is Filter of L by A2, A14, Th17;

          then

           A16: q in X1 by A13, FILTER_0: 8;

          p in X1 by A13, A15, FILTER_0: 8;

          hence p in Y & q in Y by A14, A16, TARSKI:def 4;

        end;

        then Y is Filter of L by FILTER_0: 8;

        hence thesis by A4, A6, Lm1;

      end;

      hence thesis by ZFMISC_1: 74;

    end;

    theorem :: OPENLATT:19



     Th19: not b [= a implies <.b.) in (( SF_have b) \ ( SF_have a))

    proof

      assume not b [= a;

      then not a in <.b.) by FILTER_0: 15;

      then

       A1: not <.b.) in ( SF_have a) by Th16;

      b in <.b.);

      then <.b.) in ( SF_have b);

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: OPENLATT:20



     Th20: not b [= a implies ex F st F in ( F_primeSet L) & not a in F & b in F

    proof

      set A = (( SF_have b) \ ( SF_have a));

      assume not b [= a;

      then

       A1: A <> {} by Th19;

      for Z st Z <> {} & Z c= (( SF_have b) \ ( SF_have a)) & Z is c=-linear holds ex Y st Y in (( SF_have b) \ ( SF_have a)) & for X1 st X1 in Z holds X1 c= Y by Th18;

      then

      consider Y such that

       A2: Y in A and

       A3: for Z st Z in A & Z <> Y holds not Y c= Z by A1, LATTICE4: 1;

      reconsider Y as Filter of L by A2, Th17;



       A4: b in Y by A2, Th17;



       A5: not a in Y by A2, Th17;



       A6: Y is prime

      proof

        let a1,a2 be Element of L;

        thus (a1 "\/" a2) in Y implies a1 in Y or a2 in Y

        proof

          set F2 = <.( <.a2.) \/ Y).);

          set F1 = <.( <.a1.) \/ Y).);

          assume that

           A7: (a1 "\/" a2) in Y and

           A8: not a1 in Y and

           A9: not a2 in Y;



           A10: <.a1.) c= F1 by LATTICE4: 2;

          a1 in <.a1.);

          then

           A11: a1 in F1 by A10;



           A12: Y c= F1 by LATTICE4: 2;



           A13: <.a2.) c= F2 by LATTICE4: 2;

          a2 in <.a2.);

          then

           A14: a2 in F2 by A13;



           A15: Y c= F2 by LATTICE4: 2;

           not a in F1 or not a in F2

          proof

            assume that

             A16: a in F1 and

             A17: a in F2;

            consider c1 be Element of L such that

             A18: c1 in Y and

             A19: (a1 "/\" c1) [= a by A16, LATTICE4: 3;

            consider c2 be Element of L such that

             A20: c2 in Y and

             A21: (a2 "/\" c2) [= a by A17, LATTICE4: 3;

            set c = (c1 "/\" c2);

            (a2 "/\" c) [= (a2 "/\" c2) by LATTICES: 6, LATTICES: 9;

            then

             A22: (a2 "/\" c) [= a by A21, LATTICES: 7;

            (a1 "/\" c) [= (a1 "/\" c1) by LATTICES: 6, LATTICES: 9;

            then (a1 "/\" c) [= a by A19, LATTICES: 7;

            then ((a1 "/\" c) "\/" (a2 "/\" c)) [= a by A22, FILTER_0: 6;

            then

             A23: ((a1 "\/" a2) "/\" c) [= a by LATTICES:def 11;

            c in Y by A18, A20, FILTER_0: 8;

            then ((a1 "\/" a2) "/\" c) in Y by A7, FILTER_0: 8;

            hence contradiction by A5, A23, FILTER_0: 9;

          end;

          then F1 in A or F2 in A by A4, A12, A15, Lm1;

          hence contradiction by A3, A8, A9, A11, A14, A12, A15;

        end;

        thus thesis by FILTER_0: 10;

      end;

      Y <> the carrier of L by A2, Th17;

      then Y in ( F_primeSet L) by A6;

      hence thesis by A5, A4;

    end;

    theorem :: OPENLATT:21



     Th21: a <> b implies ex F st F in ( F_primeSet L)

    proof

      assume a <> b;

      then not a [= b or not b [= a by LATTICES: 8;

      then (ex F st F in ( F_primeSet L) & not b in F & a in F) or ex F st F in ( F_primeSet L) & not a in F & b in F by Th20;

      hence thesis;

    end;

    theorem :: OPENLATT:22



     Th22: a <> b implies (( StoneH L) . a) <> (( StoneH L) . b)

    proof

      assume a <> b;

      then not a [= b or not b [= a by LATTICES: 8;

      then (ex F st F in ( F_primeSet L) & not b in F & a in F) or ex F st F in ( F_primeSet L) & not a in F & b in F by Th20;

      then

      consider F such that

       A1: F in ( F_primeSet L) and

       A2: b in F & not a in F or a in F & not b in F;

      F in (( StoneH L) . a) & not F in (( StoneH L) . b) or F in (( StoneH L) . b) & not F in (( StoneH L) . a) by A1, A2, Th11;

      hence thesis;

    end;

    registration

      let L;

      cluster ( StoneH L) -> one-to-one;

      coherence

      proof

        let x1,x2 be object;

        assume that

         A1: x1 in ( dom ( StoneH L)) and

         A2: x2 in ( dom ( StoneH L)) and

         A3: (( StoneH L) . x1) = (( StoneH L) . x2);

        reconsider a1 = x1, a2 = x2 as Element of L by A1, A2, Def6;

        a1 = a2 by A3, Th22;

        hence thesis;

      end;

    end

    definition

      let L;

      let A,B be Element of ( StoneS L);

      :: original: \/

      redefine

      func A \/ B -> Element of ( StoneS L) ;

      coherence

      proof

        consider b such that

         A1: B = (( StoneH L) . b) by Th13;

        consider a such that

         A2: A = (( StoneH L) . a) by Th13;

        (A \/ B) = (( StoneH L) . (a "\/" b)) by A2, A1, Th14;

        hence thesis by Th13;

      end;

      :: original: /\

      redefine

      func A /\ B -> Element of ( StoneS L) ;

      coherence

      proof

        consider b such that

         A3: B = (( StoneH L) . b) by Th13;

        consider a such that

         A4: A = (( StoneH L) . a) by Th13;

        (A /\ B) = (( StoneH L) . (a "/\" b)) by A4, A3, Th15;

        hence thesis by Th13;

      end;

    end

    definition

      let L;

      :: OPENLATT:def9

      func Set_Union L -> BinOp of ( StoneS L) means

      : Def9: for A,B be Element of ( StoneS L) holds (it . (A,B)) = (A \/ B);

      existence

      proof

        deffunc F( Element of ( StoneS L), Element of ( StoneS L)) = ($1 \/ $2);

        thus ex F be BinOp of ( StoneS L) st for P,Q be Element of ( StoneS L) holds (F . (P,Q)) = F(P,Q) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        set A = ( StoneS L);

        deffunc O( Element of A, Element of A) = ($1 \/ $2);

        thus for o1,o2 be BinOp of A st (for a,b be Element of A holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of A holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

      :: OPENLATT:def10

      func Set_Meet L -> BinOp of ( StoneS L) means

      : Def10: for A,B be Element of ( StoneS L) holds (it . (A,B)) = (A /\ B);

      existence

      proof

        deffunc F( Element of ( StoneS L), Element of ( StoneS L)) = ($1 /\ $2);

        thus ex F be BinOp of ( StoneS L) st for P,Q be Element of ( StoneS L) holds (F . (P,Q)) = F(P,Q) from BINOP_1:sch 4;

      end;

      uniqueness

      proof

        set A = ( StoneS L);

        deffunc O( Element of A, Element of A) = ($1 /\ $2);

        thus for o1,o2 be BinOp of A st (for a,b be Element of A holds (o1 . (a,b)) = O(a,b)) & (for a,b be Element of A holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    theorem :: OPENLATT:23



     Th23: LattStr (# ( StoneS L), ( Set_Union L), ( Set_Meet L) #) is Lattice

    proof

      set SL = LattStr (# ( StoneS L), ( Set_Union L), ( Set_Meet L) #);

       A1:

      now

        let p,q be Element of SL;



        thus (p "\/" q) = (q \/ p) by Def9

        .= (q "\/" p) by Def9;

      end;

       A2:

      now

        let p,q be Element of SL;



        thus ((p "/\" q) "\/" q) = ((p "/\" q) \/ q) by Def9

        .= ((p /\ q) \/ q) by Def10

        .= q by XBOOLE_1: 22;

      end;

       A3:

      now

        let p,q be Element of SL;



        thus (p "/\" (p "\/" q)) = (p /\ (p "\/" q)) by Def10

        .= (p /\ (p \/ q)) by Def9

        .= p by XBOOLE_1: 21;

      end;

       A4:

      now

        let p,q,r be Element of SL;



        thus (p "/\" (q "/\" r)) = (p /\ (q "/\" r)) by Def10

        .= (p /\ (q /\ r)) by Def10

        .= ((p /\ q) /\ r) by XBOOLE_1: 16

        .= ((p "/\" q) /\ r) by Def10

        .= ((p "/\" q) "/\" r) by Def10;

      end;

       A5:

      now

        let p,q be Element of SL;



        thus (p "/\" q) = (q /\ p) by Def10

        .= (q "/\" p) by Def10;

      end;

      now

        let p,q,r be Element of SL;



        thus (p "\/" (q "\/" r)) = (p \/ (q "\/" r)) by Def9

        .= (p \/ (q \/ r)) by Def9

        .= ((p \/ q) \/ r) by XBOOLE_1: 4

        .= ((p "\/" q) \/ r) by Def9

        .= ((p "\/" q) "\/" r) by Def9;

      end;

      then SL is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A2, A5, A4, A3;

      hence thesis;

    end;

    definition

      let L;

      :: OPENLATT:def11

      func StoneLatt L -> Lattice equals LattStr (# ( StoneS L), ( Set_Union L), ( Set_Meet L) #);

      coherence by Th23;

    end

    reserve p,q for Element of ( StoneLatt L);

    theorem :: OPENLATT:24

    for L holds the carrier of ( StoneLatt L) = ( StoneS L);

    theorem :: OPENLATT:25

    (p "\/" q) = (p \/ q) & (p "/\" q) = (p /\ q) by Def9, Def10;

    theorem :: OPENLATT:26

    p [= q iff p c= q

    proof

      (p "\/" q) = (p \/ q) by Def9;

      hence thesis by XBOOLE_1: 7, XBOOLE_1: 12;

    end;

    definition

      let L;

      ::$Notion-Name

      :: original: StoneH

      redefine

      func StoneH (L) -> Homomorphism of L, ( StoneLatt L) ;

      coherence

      proof

        ( dom ( StoneH L)) = the carrier of L by Def6;

        then

        reconsider f = ( StoneH L) as Function of the carrier of L, the carrier of ( StoneLatt L) by FUNCT_2: 1;

        now

          let a, b;



          thus (f . (a "\/" b)) = ((f . a) \/ (f . b)) by Th14

          .= ((f . a) "\/" (f . b)) by Def9;



          thus (f . (a "/\" b)) = ((f . a) /\ (f . b)) by Th15

          .= ((f . a) "/\" (f . b)) by Def10;

        end;

        then f is "\/"-preserving "/\"-preserving;

        hence thesis;

      end;

    end

    registration

      let L;

      cluster ( StoneH L) -> bijective;

      coherence

      proof

        ( StoneH L) is one-to-one onto;

        hence thesis;

      end;

      cluster ( StoneLatt L) -> distributive;

      coherence

      proof

        ( StoneH L) is onto;

        hence thesis by LATTICE4: 11;

      end;

    end

    theorem :: OPENLATT:27

    (L,( StoneLatt L)) are_isomorphic

    proof

      take ( StoneH L);

      thus thesis;

    end;

    registration

      cluster non trivial for H_Lattice;

      existence

      proof

        set T = the non empty TopSpace;

        set OL = ( Open_setLatt T);

        the carrier of T = ( Top OL) by Th9;

        then

        reconsider a = the carrier of T as Element of OL;

         {} = ( Bottom OL) by Th8;

        then

        reconsider b = {} as Element of OL;

        take OL, a, b;

        thus thesis;

      end;

    end

    reserve H for non trivial H_Lattice;

    reserve p9,q9 for Element of H;

    theorem :: OPENLATT:28



     Th28: (( StoneH H) . ( Top H)) = ( F_primeSet H)

    proof

      hereby

        let x be object;

        assume x in (( StoneH H) . ( Top H));

        then ex F be Filter of H st F = x & F <> the carrier of H & F is prime & ( Top H) in F by Th12;

        hence x in ( F_primeSet H);

      end;

      let x be object;

      assume x in ( F_primeSet H);

      then

      consider F be Filter of H such that

       A1: F = x and

       A2: F <> the carrier of H and

       A3: F is prime;

      ( Top H) in F by FILTER_0: 11;

      hence thesis by A1, A2, A3, Th12;

    end;

    theorem :: OPENLATT:29



     Th29: (( StoneH H) . ( Bottom H)) = {}

    proof

      set x = the Element of (( StoneH H) . ( Bottom H));

      assume (( StoneH H) . ( Bottom H)) <> {} ;

      then ex F be Filter of H st F = x & F <> the carrier of H & F is prime & ( Bottom H) in F by Th12;

      hence contradiction by FILTER_0: 26;

    end;

    theorem :: OPENLATT:30



     Th30: ( StoneS H) c= ( bool ( F_primeSet H))

    proof

      let x be object;

      reconsider xx = x as set by TARSKI: 1;

      assume x in ( StoneS H);

      then

      consider p9 such that

       A1: x = (( StoneH H) . p9) by Th13;



       A2: x = { F where F be Filter of H : F in ( F_primeSet H) & p9 in F } by A1, Def6;

      xx c= ( F_primeSet H)

      proof

        let y be object;

        assume y in xx;

        then ex F be Filter of H st y = F & F in ( F_primeSet H) & p9 in F by A2;

        hence thesis;

      end;

      hence thesis;

    end;

    registration

      let H;

      cluster ( F_primeSet H) -> non empty;

      coherence

      proof

        ex p9, q9 st p9 <> q9 by STRUCT_0:def 10;

        then ex F be Filter of H st F in ( F_primeSet H) by Th21;

        hence thesis;

      end;

    end

    definition

      let H;

      :: OPENLATT:def12

      func HTopSpace H -> strict TopStruct means

      : Def12: the carrier of it = ( F_primeSet H) & the topology of it = the set of all ( union A) where A be Subset of ( StoneS H);

      existence

      proof

        set FS = ( F_primeSet H);

        set top = the set of all ( union A) where A be Subset of ( StoneS H);



         A1: ( StoneS H) c= ( bool FS) by Th30;

        top c= ( bool FS)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in top;

          then

          consider A be Subset of ( StoneS H) such that

           A2: x = ( union A);

          A c= ( bool FS) by A1;

          then xx c= ( union ( bool FS)) by A2, ZFMISC_1: 77;

          then x is Subset of FS by ZFMISC_1: 81;

          hence thesis;

        end;

        then

        reconsider top as Subset-Family of FS;

        take TopStruct (# FS, top #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let H;

      cluster ( HTopSpace H) -> non empty TopSpace-like;

      coherence

      proof

        reconsider A1 = {(( StoneH H) . ( Top H))} as Subset of ( StoneS H);

        set TS = ( HTopSpace H);



         A1: the topology of TS = the set of all ( union A) where A be Subset of ( StoneS H) by Def12;



         A2: the carrier of TS = ( F_primeSet H) by Def12;

        hence ( HTopSpace H) is non empty;

        ( F_primeSet H) = (( StoneH H) . ( Top H)) by Th28;

        then ( F_primeSet H) = ( union A1) by ZFMISC_1: 25;

        hence the carrier of TS in the topology of TS by A2, A1;

        hereby

          let a be Subset-Family of TS;

          defpred P[ set] means ( union $1) in a;

          set B = { A where A be Subset of ( StoneS H) : P[A] };

          set X = { ( union A) where A be Subset of ( StoneS H) : A in B };

          assume

           A3: a c= the topology of TS;



           A4: a = X

          proof

            hereby

              let x be object;

              assume

               A5: x in a;

              then x in the topology of TS by A3;

              then

              consider A be Subset of ( StoneS H) such that

               A6: x = ( union A) by A1;

              A in B by A5, A6;

              hence x in X by A6;

            end;

            let x be object;

            assume x in X;

            then

            consider A be Subset of ( StoneS H) such that

             A7: x = ( union A) and

             A8: A in B;

            ex A9 be Subset of ( StoneS H) st A = A9 & ( union A9) in a by A8;

            hence thesis by A7;

          end;

          reconsider B as Subset-Family of ( StoneS H) from DOMAIN_1:sch 7;

          ( union ( union B)) = ( union a) by A4, EQREL_1: 54;

          hence ( union a) in the topology of TS by A1;

        end;

        let a,b be Subset of TS;

        assume that

         A9: a in the topology of TS and

         A10: b in the topology of TS;

        consider A be Subset of ( StoneS H) such that

         A11: a = ( union A) by A1, A9;

        consider B be Subset of ( StoneS H) such that

         A12: b = ( union B) by A1, A10;

        ( INTERSECTION (A,B)) c= ( StoneS H)

        proof

          let x be object;

          assume x in ( INTERSECTION (A,B));

          then

          consider X,Y be set such that

           A13: X in A and

           A14: Y in B and

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

          consider p9 such that

           A16: X = (( StoneH H) . p9) by A13, Th13;

          consider q9 such that

           A17: Y = (( StoneH H) . q9) by A14, Th13;

          x = (( StoneH H) . (p9 "/\" q9)) by A15, A16, A17, Th15;

          hence thesis;

        end;

        then

        reconsider C = ( INTERSECTION (A,B)) as Subset of ( StoneS H);

        (( union A) /\ ( union B)) = ( union C) by SETFAM_1: 28;

        hence thesis by A1, A11, A12;

      end;

    end

    theorem :: OPENLATT:31

    the carrier of ( Open_setLatt ( HTopSpace H)) = the set of all ( union A) where A be Subset of ( StoneS H) by Def12;

    theorem :: OPENLATT:32



     Th32: ( StoneS H) c= the carrier of ( Open_setLatt ( HTopSpace H))

    proof

      let x be object;

      set carrO = the carrier of ( Open_setLatt ( HTopSpace H));

      assume x in ( StoneS H);

      then

      reconsider z = {x} as Subset of ( StoneS H) by ZFMISC_1: 31;



       A1: ( union z) = x by ZFMISC_1: 25;

      carrO = the set of all ( union A) where A be Subset of ( StoneS H) by Def12;

      hence thesis by A1;

    end;

    definition

      let H;

      :: original: StoneH

      redefine

      func StoneH (H) -> Homomorphism of H, ( Open_setLatt ( HTopSpace H)) ;

      coherence

      proof

        set LH = ( Open_setLatt ( HTopSpace H));

        reconsider g = ( StoneH H) as Function of the carrier of H, the carrier of ( StoneLatt H);

        ( StoneS H) c= the carrier of LH by Th32;

        then

        reconsider f = g as Function of the carrier of H, the carrier of LH by FUNCT_2: 6;

        now

          let p9, q9;



          thus (f . (p9 "\/" q9)) = ((( StoneH H) . p9) \/ (( StoneH H) . q9)) by Th14

          .= ((f . p9) "\/" (f . q9)) by Def2;



          thus (f . (p9 "/\" q9)) = ((( StoneH H) . p9) /\ (( StoneH H) . q9)) by Th15

          .= ((f . p9) "/\" (f . q9)) by Def3;

        end;

        then f is "\/"-preserving "/\"-preserving;

        hence thesis;

      end;

    end

    theorem :: OPENLATT:33



     Th33: (( StoneH H) . (p9 => q9)) = ((( StoneH H) . p9) => (( StoneH H) . q9))

    proof



       A1: the carrier of ( Open_setLatt ( HTopSpace H)) = the set of all ( union A) where A be Subset of ( StoneS H) by Def12;

       A2:

      now

        let r be Element of ( Open_setLatt ( HTopSpace H));

        r in the carrier of ( Open_setLatt ( HTopSpace H));

        then

        consider A be Subset of ( StoneS H) such that

         A3: r = ( union A) by A1;

        assume ((( StoneH H) . p9) "/\" r) [= (( StoneH H) . q9);

        then ((( StoneH H) . p9) "/\" r) c= (( StoneH H) . q9) by Th6;

        then ((( StoneH H) . p9) /\ ( union A)) c= (( StoneH H) . q9) by A3, Def3;

        then

         A4: ( union ( INTERSECTION ( {(( StoneH H) . p9)},A))) c= (( StoneH H) . q9) by SETFAM_1: 25;

        now

          let x;

          assume

           A5: x in A;

          then

          consider x9 be Element of H such that

           A6: x = (( StoneH H) . x9) by Th13;

          (( StoneH H) . p9) in {(( StoneH H) . p9)} by TARSKI:def 1;

          then ((( StoneH H) . p9) /\ x) in ( INTERSECTION ( {(( StoneH H) . p9)},A)) by A5, SETFAM_1:def 5;

          then ((( StoneH H) . p9) /\ (( StoneH H) . x9)) c= (( StoneH H) . q9) by A4, A6, SETFAM_1: 41;

          then (( StoneH H) . (p9 "/\" x9)) c= (( StoneH H) . q9) by Th15;

          then (( StoneH H) . (p9 "/\" x9)) [= (( StoneH H) . q9) by Th6;

          then (p9 "/\" x9) [= q9 by LATTICE4: 5;

          then x9 [= (p9 => q9) by FILTER_0:def 7;

          then (( StoneH H) . x9) [= (( StoneH H) . (p9 => q9)) by LATTICE4: 4;

          hence x c= (( StoneH H) . (p9 => q9)) by A6, Th6;

        end;

        then ( union A) c= (( StoneH H) . (p9 => q9)) by ZFMISC_1: 76;

        hence r [= (( StoneH H) . (p9 => q9)) by A3, Th6;

      end;

      (p9 "/\" (p9 => q9)) [= q9 by FILTER_0:def 7;

      then (( StoneH H) . (p9 "/\" (p9 => q9))) [= (( StoneH H) . q9) by LATTICE4: 4;

      then ((( StoneH H) . p9) "/\" (( StoneH H) . (p9 => q9))) [= (( StoneH H) . q9) by LATTICE4:def 2;

      hence thesis by A2, FILTER_0:def 7;

    end;

    theorem :: OPENLATT:34

    ( StoneH H) preserves_implication by Th33;

    theorem :: OPENLATT:35

    ( StoneH H) preserves_top

    proof

      (( StoneH H) . ( Top H)) = ( F_primeSet H) by Th28

      .= the carrier of ( HTopSpace H) by Def12

      .= ( Top ( Open_setLatt ( HTopSpace H))) by Th9;

      hence thesis;

    end;

    theorem :: OPENLATT:36

    ( StoneH H) preserves_bottom

    proof

      (( StoneH H) . ( Bottom H)) = {} by Th29

      .= ( Bottom ( Open_setLatt ( HTopSpace H))) by Th8;

      hence thesis;

    end;