yellow13.miz



    begin

    theorem :: YELLOW13:1

    

     Th1: for T be T_1 non empty TopSpace, A be finite Subset of T holds A is closed

    proof

      let T be T_1 non empty TopSpace, A be finite Subset of T;

      defpred P[ set] means ex S be Subset of T st $1 = S & S is closed;

      

       A1: P[ {} ]

      proof

        take ( {} T);

        thus ( {} T) = {} ;

        thus thesis;

      end;

      

       A2: for x,C be set st x in A & C c= A & P[C] holds P[(C \/ {x})]

      proof

        let x,C be set;

        assume that

         A3: x in A and C c= A and

         A4: P[C];

        reconsider y = x as Element of T by A3;

        consider S be Subset of T such that

         A5: C = S and

         A6: S is closed by A4;

         {y} is closed by URYSOHN1: 19;

        then (S \/ {y}) is closed by A6;

        hence thesis by A5;

      end;

      

       A7: A is finite;

       P[A] from FINSET_1:sch 2( A7, A1, A2);

      hence thesis;

    end;

    registration

      let T be T_1 non empty TopSpace;

      cluster finite -> closed for Subset of T;

      coherence by Th1;

    end

    registration

      let T be compact TopStruct;

      cluster ( [#] T) -> compact;

      coherence by COMPTS_1: 1;

    end

    registration

      cluster finite T_1 -> discrete for non empty TopSpace;

      coherence

      proof

        let T be non empty TopSpace;

        assume T is finite T_1;

        then for A be Subset of T holds A is closed;

        hence thesis by TDLAT_3: 16;

      end;

    end

    registration

      cluster finite -> compact for TopSpace;

      coherence ;

    end

    theorem :: YELLOW13:2

    

     Th2: for T be discrete non empty TopSpace holds T is normal

    proof

      let T be discrete non empty TopSpace;

      let W,V be Subset of T such that W <> {} and V <> {} and W is closed and V is closed and

       A1: (W /\ V) = {} ;

      take P = W, Q = V;

      thus P is open & Q is open by TDLAT_3: 15;

      thus W c= P & V c= Q & (P /\ Q) = {} by A1;

    end;

    theorem :: YELLOW13:3

    

     Th3: for T be discrete non empty TopSpace holds T is regular

    proof

      let T be discrete non empty TopSpace;

      let p be Point of T, P be Subset of T such that P <> {} and P is closed and

       A1: p in (P ` );

      take W = {p}, V = P;

      thus W is open & V is open by TDLAT_3: 15;

      

       A2: not p in P by A1, XBOOLE_0:def 5;

      (W /\ V) c= {}

      proof

        let a be object;

        assume

         A3: a in (W /\ V);

        assume not a in {} ;

        a in W & a in V by A3, XBOOLE_0:def 4;

        hence contradiction by A2, TARSKI:def 1;

      end;

      hence p in W & P c= V & (W /\ V) = {} by TARSKI:def 1;

    end;

    theorem :: YELLOW13:4

    

     Th4: for T be discrete non empty TopSpace holds T is T_2

    proof

      let T be discrete non empty TopSpace;

      let p,q be Point of T such that

       A1: not p = q;

      take W = {p}, V = {q};

      thus W is open & V is open by TDLAT_3: 15;

      (W /\ V) c= {}

      proof

        let a be object;

        assume

         A2: a in (W /\ V);

        then a in W by XBOOLE_0:def 4;

        then

         A3: a = p by TARSKI:def 1;

        assume not a in {} ;

        a in V by A2, XBOOLE_0:def 4;

        hence contradiction by A1, A3, TARSKI:def 1;

      end;

      hence p in W & q in V & (W /\ V) = {} by TARSKI:def 1;

    end;

    theorem :: YELLOW13:5

    

     Th5: for T be discrete non empty TopSpace holds T is T_1

    proof

      let T be discrete non empty TopSpace;

      for p be Point of T holds {p} is closed by TDLAT_3: 16;

      hence thesis by URYSOHN1: 19;

    end;

    registration

      cluster discrete non empty -> normal regular T_2 T_1 for TopSpace;

      coherence by Th2, Th3, Th4, Th5;

    end

    registration

      cluster T_4 -> regular for non empty TopSpace;

      coherence

      proof

        let T be non empty TopSpace such that

         A1: T is T_4;

        let p be Point of T, P be Subset of T such that

         A2: P <> {} & P is closed and

         A3: p in (P ` );

        

         A4: not p in P by A3, XBOOLE_0:def 5;

        (P /\ {p}) c= {}

        proof

          let a be object;

          assume

           A5: a in (P /\ {p});

          assume not a in {} ;

          a in P & a in {p} by A5, XBOOLE_0:def 4;

          hence contradiction by A4, TARSKI:def 1;

        end;

        then (P /\ {p}) = {} ;

        then P misses {p};

        then

        consider R,Q be Subset of T such that

         A6: R is open & Q is open & {p} c= R & P c= Q & R misses Q by A1, A2, COMPTS_1:def 3;

        take R, Q;

        p in {p} by TARSKI:def 1;

        hence thesis by A6;

      end;

    end

    registration

      cluster T_3 -> T_2 for TopSpace;

      coherence

      proof

        let T be TopSpace such that

         A1: T is T_3;

        let p,q be Point of T;

        assume

         A2: p <> q;

        then

         A3: not p in {q} by TARSKI:def 1;

        now

          assume

           A4: the carrier of T = {} ;

          then p = {} by SUBSET_1:def 1;

          hence contradiction by A2, A4, SUBSET_1:def 1;

        end;

        then

        reconsider T9 = T as non empty TopSpace;

        reconsider p, q as Point of T9;

        p in ( {q} ` ) by A3, SUBSET_1: 29;

        then

        consider W,V be Subset of T such that

         A5: W is open & V is open & p in W & {q} c= V & W misses V by A1, COMPTS_1:def 2;

        take W, V;

        q in {q} by TARSKI:def 1;

        hence thesis by A5;

      end;

    end

    theorem :: YELLOW13:6

    

     Th6: for S be reflexive RelStr, T be reflexive transitive RelStr, f be Function of S, T, X be Subset of S holds ( downarrow (f .: X)) c= ( downarrow (f .: ( downarrow X)))

    proof

      let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function of S, T, X be Subset of S;

      (f .: X) c= (f .: ( downarrow X)) by RELAT_1: 123, WAYBEL_0: 16;

      hence thesis by YELLOW_3: 6;

    end;

    theorem :: YELLOW13:7

    for S be reflexive RelStr, T be reflexive transitive RelStr, f be Function of S, T, X be Subset of S st f is monotone holds ( downarrow (f .: X)) = ( downarrow (f .: ( downarrow X)))

    proof

      let S be reflexive RelStr, T be reflexive transitive RelStr, f be Function of S, T, X be Subset of S such that

       A1: f is monotone;

      thus ( downarrow (f .: X)) c= ( downarrow (f .: ( downarrow X))) by Th6;

      let a be object;

      assume

       A2: a in ( downarrow (f .: ( downarrow X)));

      then

      reconsider T1 = T as non empty reflexive transitive RelStr;

      reconsider b = a as Element of T1 by A2;

      consider fx be Element of T1 such that

       A3: fx >= b and

       A4: fx in (f .: ( downarrow X)) by A2, WAYBEL_0:def 15;

      consider x be object such that

       A5: x in ( dom f) and

       A6: x in ( downarrow X) and

       A7: fx = (f . x) by A4, FUNCT_1:def 6;

      reconsider S1 = S as non empty reflexive RelStr by A5;

      reconsider x as Element of S1 by A5;

      consider y be Element of S1 such that

       A8: y >= x and

       A9: y in X by A6, WAYBEL_0:def 15;

      reconsider f1 = f as Function of S1, T1;

      (f1 . x) <= (f1 . y) by A1, A8, ORDERS_3:def 5;

      then

       A10: b <= (f1 . y) by A3, A7, ORDERS_2: 3;

      the carrier of T1 <> {} ;

      then ( dom f) = the carrier of S by FUNCT_2:def 1;

      then (f . y) in (f .: X) by A9, FUNCT_1:def 6;

      hence thesis by A10, WAYBEL_0:def 15;

    end;

    theorem :: YELLOW13:8

    

     Th8: for N be non empty Poset holds ( IdsMap N) is one-to-one

    proof

      let N be non empty Poset;

      set f = ( IdsMap N);

      let x,y be Element of N such that

       A1: (f . x) = (f . y);

      (f . x) = ( downarrow x) & (f . y) = ( downarrow y) by YELLOW_2:def 4;

      hence thesis by A1, WAYBEL_0: 19;

    end;

    registration

      let N be non empty Poset;

      cluster ( IdsMap N) -> one-to-one;

      coherence by Th8;

    end

    theorem :: YELLOW13:9

    

     Th9: for N be finite LATTICE holds ( SupMap N) is one-to-one

    proof

      let N be finite LATTICE;

      set f = ( SupMap N);

      let x,y be Element of ( InclPoset ( Ids N)) such that

       A1: (f . x) = (f . y);

      reconsider X = x, Y = y as Ideal of N by YELLOW_2: 41;

      

       A2: (f . x) = ( sup X) & (f . y) = ( sup Y) by YELLOW_2:def 3;

      X = Y

      proof

        hereby

          let a be object;

          

           A3: ( sup Y) in Y by WAYBEL_3: 16;

          assume

           A4: a in X;

          then

          reconsider b = a as Element of N;

          b <= ( sup Y) by A1, A2, A4, YELLOW_0: 17, YELLOW_4: 1;

          hence a in Y by A3, WAYBEL_0:def 19;

        end;

        let a be object;

        

         A5: ( sup X) in X by WAYBEL_3: 16;

        assume

         A6: a in Y;

        then

        reconsider b = a as Element of N;

        b <= ( sup X) by A1, A2, A6, YELLOW_0: 17, YELLOW_4: 1;

        hence thesis by A5, WAYBEL_0:def 19;

      end;

      hence thesis;

    end;

    registration

      let N be finite LATTICE;

      cluster ( SupMap N) -> one-to-one;

      coherence by Th9;

    end

    theorem :: YELLOW13:10

    for N be finite LATTICE holds (N,( InclPoset ( Ids N))) are_isomorphic

    proof

      let N be finite LATTICE;

      set I = ( InclPoset ( Ids N));

      take i = ( IdsMap N);

      N is non empty & I is non empty implies i is one-to-one monotone & ex s be Function of I, N st s = (i " ) & s is monotone

      proof

        assume that N is non empty and I is non empty;

        thus i is one-to-one monotone;

        take s = ( SupMap N);

         [i, s] is Galois by WAYBEL_1: 57;

        then i is onto by WAYBEL_1: 24;

        then

         A1: ( rng i) = the carrier of I by FUNCT_2:def 3;

        

         A2: for y,x be object holds y in ( rng i) & x = (s . y) iff x in ( dom i) & y = (i . x)

        proof

          let y,x be object;

          

           A3: ( dom i) = the carrier of N by FUNCT_2:def 1;

          hereby

            assume that

             A4: y in ( rng i) and

             A5: x = (s . y);

            reconsider Y = y as Element of I by A4;

            x = (s . Y) by A5;

            hence x in ( dom i) by A3;

            reconsider Y1 = Y as Ideal of N by YELLOW_2: 41;

            

            thus (i . x) = (i . ( sup Y1)) by A5, YELLOW_2:def 3

            .= ( downarrow ( sup Y1)) by YELLOW_2:def 4

            .= y by WAYBEL14: 5, WAYBEL_3: 16;

          end;

          assume that

           A6: x in ( dom i) and

           A7: y = (i . x);

          reconsider X = x as Element of N by A6;

          

           A8: y = (i . X) by A7;

          then

          reconsider Y = y as Ideal of N by YELLOW_2: 41;

          thus y in ( rng i) by A1, A8;

          

          thus (s . y) = ( sup Y) by YELLOW_2:def 3

          .= ( sup ( downarrow X)) by A7, YELLOW_2:def 4

          .= x by WAYBEL_0: 34;

        end;

        ( dom s) = the carrier of I by FUNCT_2:def 1;

        hence s = (i " ) by A1, A2, FUNCT_1: 32;

        thus thesis;

      end;

      hence thesis by WAYBEL_0:def 38;

    end;

    theorem :: YELLOW13:11

    

     Th11: for N be complete non empty Poset, x be Element of N, X be non empty Subset of N holds (x "/\" ) preserves_inf_of X

    proof

      let N be complete non empty Poset, x be Element of N, X be non empty Subset of N such that

       A1: ex_inf_of (X,N);

      

       A2: for b be Element of N st b is_<=_than ((x "/\" ) .: X) holds ((x "/\" ) . ( inf X)) >= b

      proof

        consider y be object such that

         A3: y in X by XBOOLE_0:def 1;

        reconsider y as Element of N by A3;

        let b be Element of N such that

         A4: b is_<=_than ((x "/\" ) .: X);

        

         A5: ((x "/\" ) .: X) = { (x "/\" z) where z be Element of N : z in X } by WAYBEL_1: 61;

        then (x "/\" y) in ((x "/\" ) .: X) by A3;

        then

         A6: b <= (x "/\" y) by A4;

        X is_>=_than b

        proof

          let c be Element of N;

          assume c in X;

          then (x "/\" c) in ((x "/\" ) .: X) by A5;

          then

           A7: b <= (x "/\" c) by A4;

          (x "/\" c) <= c by YELLOW_0: 23;

          hence b <= c by A7, ORDERS_2: 3;

        end;

        then

         A8: b <= ( inf X) by A1, YELLOW_0:def 10;

        (x "/\" y) <= x by YELLOW_0: 23;

        then b <= x by A6, ORDERS_2: 3;

        then (b "/\" b) <= (x "/\" ( inf X)) by A8, YELLOW_3: 2;

        then b <= (x "/\" ( inf X)) by YELLOW_0: 25;

        hence b <= ((x "/\" ) . ( inf X)) by WAYBEL_1:def 18;

      end;

      thus ex_inf_of (((x "/\" ) .: X),N) by YELLOW_0: 17;

      ( inf X) is_<=_than X by A1, YELLOW_0:def 10;

      then ((x "/\" ) . ( inf X)) is_<=_than ((x "/\" ) .: X) by YELLOW_2: 13;

      hence thesis by A2, YELLOW_0: 33;

    end;

    theorem :: YELLOW13:12

    

     Th12: for N be complete non empty Poset, x be Element of N holds (x "/\" ) is meet-preserving

    proof

      let N be complete non empty Poset, x be Element of N;

      let a,b be Element of N;

      thus thesis by Th11;

    end;

    registration

      let N be complete non empty Poset, x be Element of N;

      cluster (x "/\" ) -> meet-preserving;

      coherence by Th12;

    end

    begin

    theorem :: YELLOW13:13

    for T be anti-discrete non empty TopStruct, p be Point of T holds {the carrier of T} is Basis of p

    proof

      let T be anti-discrete non empty TopStruct, p be Point of T;

      set A = {the carrier of T};

      A c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in A;

        then

         A1: a = the carrier of T by TARSKI:def 1;

        the carrier of T c= the carrier of T;

        hence thesis by A1;

      end;

      then

      reconsider A as Subset-Family of T;

      A is Basis of p

      proof

        

         A2: A is open

        proof

          let a be Subset of T;

          assume a in A;

          then a = ( [#] T) by TARSKI:def 1;

          hence thesis;

        end;

        A is p -quasi_basis

        proof

          ( Intersect A) = ( meet A) by SETFAM_1:def 9

          .= the carrier of T by SETFAM_1: 10;

          hence p in ( Intersect A);

          let S be Subset of T;

          assume S is open & p in S;

          then

           A3: S = the carrier of T by TDLAT_3: 18;

          take S;

          thus thesis by A3, TARSKI:def 1;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: YELLOW13:14

    for T be anti-discrete non empty TopStruct, p be Point of T, D be Basis of p holds D = {the carrier of T}

    proof

      let T be anti-discrete non empty TopStruct, p be Point of T, D be Basis of p;

      thus D c= {the carrier of T}

      proof

        let a be object;

        assume

         A1: a in D;

        then

        reconsider X = a as Subset of T;

        X is open & p in X by A1, YELLOW_8: 12;

        then X = the carrier of T by TDLAT_3: 18;

        hence thesis by TARSKI:def 1;

      end;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: YELLOW13:15

    for T be non empty TopSpace, P be Basis of T, p be Point of T holds { A where A be Subset of T : A in P & p in A } is Basis of p

    proof

      let T be non empty TopSpace, P be Basis of T, p be Point of T;

      set Z = { A where A be Subset of T : A in P & p in A };

      Z c= ( bool the carrier of T)

      proof

        let z be object;

        assume z in Z;

        then ex A be Subset of T st A = z & A in P & p in A;

        hence thesis;

      end;

      then

      reconsider Z as Subset-Family of T;

      reconsider Z as Subset-Family of T;

      Z is Basis of p

      proof

        

         A1: Z is open

        proof

          let z be Subset of T;

          assume z in Z;

          then

          consider A be Subset of T such that

           A2: A = z and

           A3: A in P and p in A;

          A is open by A3, YELLOW_8: 10;

          hence thesis by A2;

        end;

        Z is p -quasi_basis

        proof

          now

            let z be set;

            assume z in Z;

            then ex A be Subset of T st A = z & A in P & p in A;

            hence p in z;

          end;

          hence p in ( Intersect Z) by SETFAM_1: 43;

          let S be Subset of T;

          assume S is open & p in S;

          then

          consider V be Subset of T such that

           A4: V in P & p in V & V c= S by YELLOW_9: 31;

          take V;

          thus thesis by A4;

        end;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    

     Lm1: for T be non empty TopStruct, A be Subset of T, p be Point of T st p in ( Cl A) holds for K be Basis of p, Q be Subset of T st Q in K holds A meets Q

    proof

      let T be non empty TopStruct, A be Subset of T, p be Point of T such that

       A1: p in ( Cl A);

      let K be Basis of p, Q be Subset of T;

      assume Q in K;

      then Q is open & p in Q by YELLOW_8: 12;

      then A meets Q by A1, PRE_TOPC:def 7;

      hence (A /\ Q) <> {} ;

    end;

    

     Lm2: for T be non empty TopStruct, A be Subset of T, p be Point of T st for K be Basis of p, Q be Subset of T st Q in K holds A meets Q holds ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q

    proof

      let T be non empty TopStruct, A be Subset of T, p be Point of T such that

       A1: for K be Basis of p, Q be Subset of T st Q in K holds A meets Q and

       A2: for K be Basis of p holds ex Q be Subset of T st Q in K & A misses Q;

      set K = the Basis of p;

      ex Q be Subset of T st Q in K & A misses Q by A2;

      hence contradiction by A1;

    end;

    

     Lm3: for T be non empty TopStruct, A be Subset of T, p be Point of T st ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q holds p in ( Cl A)

    proof

      let T be non empty TopStruct, A be Subset of T, p be Point of T;

      given K be Basis of p such that

       A1: for Q be Subset of T st Q in K holds A meets Q;

      assume not p in ( Cl A);

      then

      consider F be Subset of T such that

       A2: F is closed and

       A3: A c= F and

       A4: not p in F by PRE_TOPC: 15;

      

       A5: A misses (F ` ) by A3, SUBSET_1: 24;

      p in (F ` ) & (F ` ) is open by A2, A4, XBOOLE_0:def 5;

      then

      consider W be Subset of T such that

       A6: W in K and

       A7: W c= (F ` ) by YELLOW_8: 13;

      A meets W by A1, A6;

      hence contradiction by A7, A5, XBOOLE_1: 63;

    end;

    theorem :: YELLOW13:16

    for T be non empty TopStruct, A be Subset of T, p be Point of T holds p in ( Cl A) iff for K be Basis of p, Q be Subset of T st Q in K holds A meets Q

    proof

      let T be non empty TopStruct, A be Subset of T, p be Point of T;

      thus p in ( Cl A) implies for K be Basis of p, Q be Subset of T st Q in K holds A meets Q by Lm1;

      assume for K be Basis of p, Q be Subset of T st Q in K holds A meets Q;

      then ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q by Lm2;

      hence thesis by Lm3;

    end;

    theorem :: YELLOW13:17

    for T be non empty TopStruct, A be Subset of T, p be Point of T holds p in ( Cl A) iff ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q

    proof

      let T be non empty TopStruct, A be Subset of T, p be Point of T;

      hereby

        assume p in ( Cl A);

        then for K be Basis of p, Q be Subset of T st Q in K holds A meets Q by Lm1;

        hence ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q by Lm2;

      end;

      assume ex K be Basis of p st for Q be Subset of T st Q in K holds A meets Q;

      hence thesis by Lm3;

    end;

    definition

      let T be TopStruct, p be Point of T;

      :: YELLOW13:def1

      mode basis of p -> Subset-Family of T means

      : Def1: for A be Subset of T st p in ( Int A) holds ex P be Subset of T st P in it & p in ( Int P) & P c= A;

      existence

      proof

        reconsider F = ( bool the carrier of T) as Subset-Family of T;

        reconsider F as Subset-Family of T;

        take F;

        let A be Subset of T such that

         A1: p in ( Int A);

        take ( Int A);

        thus thesis by A1, TOPS_1: 16;

      end;

    end

    definition

      let T be non empty TopSpace, p be Point of T;

      :: original: basis

      redefine

      :: YELLOW13:def2

      mode basis of p means for A be a_neighborhood of p holds ex P be a_neighborhood of p st P in it & P c= A;

      compatibility

      proof

        let F be Subset-Family of T;

        hereby

          assume

           A1: F is basis of p;

          let A be a_neighborhood of p;

          p in ( Int A) by CONNSP_2:def 1;

          then

          consider P be Subset of T such that

           A2: P in F and

           A3: p in ( Int P) and

           A4: P c= A by A1, Def1;

          reconsider P as a_neighborhood of p by A3, CONNSP_2:def 1;

          take P;

          thus P in F & P c= A by A2, A4;

        end;

        assume

         A5: for A be a_neighborhood of p holds ex P be a_neighborhood of p st P in F & P c= A;

        let A be Subset of T;

        assume p in ( Int A);

        then A is a_neighborhood of p by CONNSP_2:def 1;

        then

        consider P be a_neighborhood of p such that

         A6: P in F & P c= A by A5;

        take P;

        thus thesis by A6, CONNSP_2:def 1;

      end;

    end

    theorem :: YELLOW13:18

    

     Th18: for T be TopStruct, p be Point of T holds ( bool the carrier of T) is basis of p

    proof

      let T be TopStruct, p be Point of T;

      reconsider F = ( bool the carrier of T) as Subset-Family of T;

      reconsider F as Subset-Family of T;

      F is basis of p

      proof

        let A be Subset of T such that

         A1: p in ( Int A);

        take ( Int A);

        thus thesis by A1, TOPS_1: 16;

      end;

      hence thesis;

    end;

    theorem :: YELLOW13:19

    

     Th19: for T be non empty TopSpace, p be Point of T, P be basis of p holds P is non empty

    proof

      let T be non empty TopSpace, p be Point of T, P be basis of p;

      ( Int ( [#] T)) = ( [#] T) by TOPS_1: 15;

      then ex W be Subset of T st W in P & p in ( Int W) & W c= ( [#] T) by Def1;

      hence thesis;

    end;

    registration

      let T be non empty TopSpace, p be Point of T;

      cluster -> non empty for basis of p;

      coherence by Th19;

    end

    registration

      let T be TopStruct, p be Point of T;

      cluster non empty for basis of p;

      existence

      proof

        ( bool the carrier of T) is basis of p by Th18;

        hence thesis;

      end;

    end

    definition

      let T be TopStruct, p be Point of T, P be basis of p;

      :: YELLOW13:def3

      attr P is correct means

      : Def3: for A be Subset of T holds A in P iff p in ( Int A);

    end

     Lm4:

    now

      let T be TopStruct, p be Point of T;

      let K be set such that

       A1: K = { A where A be Subset of T : p in ( Int A) };

      K c= ( bool the carrier of T)

      proof

        let y be object;

        assume y in K;

        then ex A be Subset of T st y = A & p in ( Int A) by A1;

        hence thesis;

      end;

      then

      reconsider J = K as Subset-Family of T;

      reconsider J as Subset-Family of T;

      for A be Subset of T st p in ( Int A) holds ex P be Subset of T st P in J & p in ( Int P) & P c= A

      proof

        let A be Subset of T such that

         A2: p in ( Int A);

        take P = A;

        thus thesis by A1, A2;

      end;

      hence K is basis of p by Def1;

    end;

     Lm5:

    now

      let T be TopStruct, p be Point of T, K be basis of p such that

       A1: K = { A where A be Subset of T : p in ( Int A) };

      thus K is correct

      proof

        let A be Subset of T;

        hereby

          assume A in K;

          then ex M be Subset of T st A = M & p in ( Int M) by A1;

          hence p in ( Int A);

        end;

        thus thesis by A1;

      end;

    end;

    registration

      let T be TopStruct, p be Point of T;

      cluster correct for basis of p;

      existence

      proof

        reconsider P = { A where A be Subset of T : p in ( Int A) } as basis of p by Lm4;

        take P;

        thus thesis by Lm5;

      end;

    end

    theorem :: YELLOW13:20

    for T be TopStruct, p be Point of T holds { A where A be Subset of T : p in ( Int A) } is correct basis of p by Lm4, Lm5;

    registration

      let T be non empty TopSpace, p be Point of T;

      cluster non empty correct for basis of p;

      existence

      proof

        reconsider K = { A where A be Subset of T : p in ( Int A) } as correct basis of p by Lm4, Lm5;

        take K;

        thus thesis;

      end;

    end

    theorem :: YELLOW13:21

    for T be anti-discrete non empty TopStruct, p be Point of T holds {the carrier of T} is correct basis of p

    proof

      let T be anti-discrete non empty TopStruct, p be Point of T;

      set A = {the carrier of T};

      A c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in A;

        then

         A1: a = the carrier of T by TARSKI:def 1;

        the carrier of T c= the carrier of T;

        hence thesis by A1;

      end;

      then

      reconsider A as Subset-Family of T;

      reconsider A as Subset-Family of T;

      A is basis of p

      proof

        let S be a_neighborhood of p;

        take S;

        p in ( Int S) by CONNSP_2:def 1;

        then

         A2: ( Int S) = the carrier of T by TDLAT_3: 18;

        ( Int S) c= S by TOPS_1: 16;

        then ( Int S) = S by A2;

        hence thesis by A2, TARSKI:def 1;

      end;

      then

      reconsider A as basis of p;

      A is correct

      proof

        let X be Subset of T;

        hereby

          assume X in A;

          then X = the carrier of T by TARSKI:def 1;

          then ( Int X) = ( [#] T) by TOPS_1: 15;

          hence p in ( Int X);

        end;

        assume p in ( Int X);

        then

         A3: ( Int X) = the carrier of T by TDLAT_3: 18;

        ( Int X) c= X by TOPS_1: 16;

        then ( Int X) = X by A3;

        hence thesis by A3, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: YELLOW13:22

    for T be anti-discrete non empty TopStruct, p be Point of T, D be correct basis of p holds D = {the carrier of T}

    proof

      let T be anti-discrete non empty TopStruct, p be Point of T, D be correct basis of p;

      thus D c= {the carrier of T}

      proof

        let a be object;

        assume

         A1: a in D;

        then

        reconsider X = a as Subset of T;

        p in ( Int X) by A1, Def3;

        then

         A2: ( Int X) = the carrier of T by TDLAT_3: 18;

        ( Int X) c= X by TOPS_1: 16;

        then ( Int X) = X by A2;

        hence thesis by A2, TARSKI:def 1;

      end;

      hence thesis by ZFMISC_1: 33;

    end;

    theorem :: YELLOW13:23

    for T be non empty TopSpace, p be Point of T, P be Basis of p holds P is basis of p

    proof

      let T be non empty TopSpace, p be Point of T, P be Basis of p;

      now

        let A be Subset of T;

        assume p in ( Int A);

        then

        consider V be Subset of T such that

         A1: V in P and

         A2: V c= ( Int A) by YELLOW_8:def 1;

        take V;

        V is open by A1, YELLOW_8: 12;

        then ( Int A) c= A & ( Int V) = V by TOPS_1: 16, TOPS_1: 23;

        hence V in P & p in ( Int V) & V c= A by A1, A2, YELLOW_8: 12;

      end;

      hence thesis by Def1;

    end;

    definition

      let T be TopStruct;

      :: YELLOW13:def4

      mode basis of T -> Subset-Family of T means

      : Def4: for p be Point of T holds it is basis of p;

      existence

      proof

        reconsider F = ( bool the carrier of T) as Subset-Family of T;

        reconsider F as Subset-Family of T;

        take F;

        thus thesis by Th18;

      end;

    end

    theorem :: YELLOW13:24

    

     Th24: for T be TopStruct holds ( bool the carrier of T) is basis of T

    proof

      let T be TopStruct;

      reconsider P = ( bool the carrier of T) as Subset-Family of T;

      reconsider P as Subset-Family of T;

      P is basis of T

      proof

        let p be Point of T;

        thus thesis by Th18;

      end;

      hence thesis;

    end;

    theorem :: YELLOW13:25

    

     Th25: for T be non empty TopSpace, P be basis of T holds P is non empty

    proof

      let T be non empty TopSpace, P be basis of T;

      set p = the Point of T;

      reconsider C = P as basis of p by Def4;

      C is non empty;

      hence thesis;

    end;

    registration

      let T be non empty TopSpace;

      cluster -> non empty for basis of T;

      coherence by Th25;

    end

    registration

      let T be TopStruct;

      cluster non empty for basis of T;

      existence

      proof

        ( bool the carrier of T) is basis of T by Th24;

        hence thesis;

      end;

    end

    theorem :: YELLOW13:26

    for T be non empty TopSpace, P be basis of T holds the topology of T c= ( UniCl ( Int P))

    proof

      let T be non empty TopSpace, P be basis of T;

      let x be object;

      assume

       A1: x in the topology of T;

      then

      reconsider X = x as Subset of T;

      ex Y be Subset-Family of T st Y c= ( Int P) & X = ( union Y)

      proof

        set Y = { A where A be Subset of T : A in ( Int P) & ( Int A) c= X };

        Y c= ( bool the carrier of T)

        proof

          let y be object;

          assume y in Y;

          then ex A be Subset of T st y = A & A in ( Int P) & ( Int A) c= X;

          hence thesis;

        end;

        then

        reconsider Y as Subset-Family of T;

        reconsider Y as Subset-Family of T;

        take Y;

        hereby

          let y be object;

          assume y in Y;

          then ex A be Subset of T st y = A & A in ( Int P) & ( Int A) c= X;

          hence y in ( Int P);

        end;

        hereby

          let y be object;

          assume

           A2: y in X;

          then

          reconsider p = y as Point of T;

          reconsider C = P as basis of p by Def4;

          X is open by A1;

          then p in ( Int X) by A2, TOPS_1: 23;

          then

          consider W be Subset of T such that

           A3: W in C and

           A4: p in ( Int W) and

           A5: W c= X by Def1;

          ( Int W) c= W by TOPS_1: 16;

          then

           A6: ( Int ( Int W)) c= X by A5;

          ( Int W) in ( Int P) by A3, TDLAT_2:def 1;

          then ( Int W) in Y by A6;

          hence y in ( union Y) by A4, TARSKI:def 4;

        end;

        let y be object;

        assume y in ( union Y);

        then

        consider K be set such that

         A7: y in K and

         A8: K in Y by TARSKI:def 4;

        consider A be Subset of T such that

         A9: A = K and

         A10: A in ( Int P) and

         A11: ( Int A) c= X by A8;

        reconsider A as Subset of T;

        ex E be Subset of T st A = ( Int E) & E in P by A10, TDLAT_2:def 1;

        hence thesis by A7, A9, A11;

      end;

      hence thesis by CANTOR_1:def 1;

    end;

    theorem :: YELLOW13:27

    for T be TopSpace, P be Basis of T holds P is basis of T

    proof

      let T be TopSpace, P be Basis of T;

      

       A1: P c= the topology of T by TOPS_2: 64;

      let p be Point of T, A be Subset of T such that

       A2: p in ( Int A);

      the topology of T c= ( UniCl P) & ( Int A) in the topology of T by CANTOR_1:def 2, PRE_TOPC:def 2;

      then

      consider Y be Subset-Family of T such that

       A3: Y c= P and

       A4: ( Int A) = ( union Y) by CANTOR_1:def 1;

      reconsider Y as Subset-Family of T;

      consider K be set such that

       A5: p in K and

       A6: K in Y by A2, A4, TARSKI:def 4;

      reconsider K as Subset of T by A6;

      take K;

      thus K in P by A3, A6;

      then K is open by A1;

      hence p in ( Int K) by A5, TOPS_1: 23;

      

       A7: ( Int A) c= A by TOPS_1: 16;

      K c= ( union Y) by A6, ZFMISC_1: 74;

      hence thesis by A4, A7;

    end;

    definition

      let T be non empty TopSpace-like TopRelStr;

      :: YELLOW13:def5

      attr T is topological_semilattice means

      : Def5: for f be Function of [:T, T qua TopSpace:], T st f = ( inf_op T) holds f is continuous;

    end

    registration

      cluster reflexive -> topological_semilattice for 1 -element TopSpace-like TopRelStr;

      coherence

      proof

        let T be 1 -element TopSpace-like TopRelStr;

        assume T is reflexive;

        then

        reconsider W = T as reflexive1 -element TopSpace-like TopRelStr;

        consider d be Element of W such that

         A1: the carrier of W = {d} by TEX_1:def 1;

        let f be Function of [:T, T qua TopSpace:], T such that

         A2: f = ( inf_op T);

        now

          let P1 be Subset of T such that P1 is closed;

          per cases by TDLAT_3: 19;

            suppose P1 = {} ;

            then (f " P1) = ( {} [:T, T qua TopSpace:]);

            hence (f " P1) is closed;

          end;

            suppose

             A3: P1 = the carrier of W;

            

             A4: ( dom f) = the carrier of [:T, T qua TopSpace:] by FUNCT_2:def 1

            .= [:the carrier of T, the carrier of T:] by BORSUK_1:def 2;

            

             A5: (f " P1) = [: {d}, {d}:]

            proof

              thus for x be object st x in (f " P1) holds x in [: {d}, {d}:] by A1, A4, FUNCT_1:def 7;

              let x be object;

              

               A6: [d, d] in [:the carrier of T, the carrier of T:] by ZFMISC_1: 87;

              assume x in [: {d}, {d}:];

              then x in { [d, d]} by ZFMISC_1: 29;

              then

               A7: x = [d, d] by TARSKI:def 1;

              (f . (d,d)) = (d "/\" d) by A2, WAYBEL_2:def 4

              .= d by YELLOW_0: 25;

              hence thesis by A3, A4, A7, A6, FUNCT_1:def 7;

            end;

            ( [#] [:T, T qua TopSpace:]) = [: {d}, {d}:] by A1, BORSUK_1:def 2;

            hence (f " P1) is closed by A5;

          end;

        end;

        hence thesis;

      end;

    end

    theorem :: YELLOW13:28

    

     Th28: for T be topological_semilattice non empty TopSpace-like TopRelStr, x be Element of T holds (x "/\" ) is continuous

    proof

      let T be topological_semilattice non empty TopSpace-like TopRelStr, x be Element of T;

      let p be Point of T, G be a_neighborhood of ((x "/\" ) . p);

      set TT = [:T, T qua TopSpace:];

      

       A1: the carrier of TT = [:the carrier of T, the carrier of T:] by BORSUK_1:def 2;

      then

      reconsider xp = [x, p] as Point of TT by YELLOW_3:def 2;

      the carrier of [:T, T:] = [:the carrier of T, the carrier of T:] by YELLOW_3:def 2;

      then

      reconsider f = ( inf_op T) as Function of TT, T by A1;

      

       A2: (f . xp) = (f . (x,p))

      .= (x "/\" p) by WAYBEL_2:def 4;

      G is a_neighborhood of (x "/\" p) & f is continuous by Def5, WAYBEL_1:def 18;

      then

      consider H be a_neighborhood of xp such that

       A3: (f .: H) c= G by A2;

      consider A be Subset-Family of TT such that

       A4: ( Int H) = ( union A) and

       A5: for e be set st e in A holds ex X1,Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

      xp in ( Int H) by CONNSP_2:def 1;

      then

      consider Z be set such that

       A6: xp in Z and

       A7: Z in A by A4, TARSKI:def 4;

      consider X1,Y1 be Subset of T such that

       A8: Z = [:X1, Y1:] and X1 is open and

       A9: Y1 is open by A5, A7;

      p in Y1 by A6, A8, ZFMISC_1: 87;

      then

      reconsider Y1 as a_neighborhood of p by A9, CONNSP_2: 3;

      take Y1;

      let b be object;

      assume b in ((x "/\" ) .: Y1);

      then

      consider a be object such that a in ( dom (x "/\" )) and

       A10: a in Y1 and

       A11: b = ((x "/\" ) . a) by FUNCT_1:def 6;

      reconsider a as Element of T by A10;

      x in X1 by A6, A8, ZFMISC_1: 87;

      then [x, a] in Z by A8, A10, ZFMISC_1: 87;

      then

       A12: [x, a] in ( Int H) by A4, A7, TARSKI:def 4;

       [x, a] in [:the carrier of T, the carrier of T:] by ZFMISC_1: 87;

      then

       A13: ( Int H) c= H & [x, a] in ( dom f) by A1, FUNCT_2:def 1, TOPS_1: 16;

      b = (x "/\" a) by A11, WAYBEL_1:def 18

      .= (f . (x,a)) by WAYBEL_2:def 4;

      then b in (f .: H) by A12, A13, FUNCT_1:def 6;

      hence thesis by A3;

    end;

    registration

      let T be topological_semilattice non empty TopSpace-like TopRelStr, x be Element of T;

      cluster (x "/\" ) -> continuous;

      coherence by Th28;

    end