waybel19.miz



    begin

    definition

      let T be non empty TopRelStr;

      :: WAYBEL19:def1

      attr T is lower means

      : Def1: the set of all (( uparrow x) ` ) where x be Element of T is prebasis of T;

    end

     Lm1:

    now

      let LL,T be non empty RelStr such that

       A1: the RelStr of LL = the RelStr of T;

      set BB = the set of all (( uparrow x) ` ) where x be Element of T;

      set A = the set of all (( uparrow x) ` ) where x be Element of LL;

      thus A = BB

      proof

        hereby

          let a be object;

          assume a in A;

          then

          consider x be Element of LL such that

           A2: a = (( uparrow x) ` );

          reconsider y = x as Element of T by A1;

          a = (( uparrow y) ` ) by A1, A2, WAYBEL_0: 13;

          hence a in BB;

        end;

        let a be object;

        assume a in BB;

        then

        consider x be Element of T such that

         A3: a = (( uparrow x) ` );

        reconsider y = x as Element of LL by A1;

        a = (( uparrow y) ` ) by A1, A3, WAYBEL_0: 13;

        hence thesis;

      end;

    end;

    registration

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

      coherence

      proof

        let T be 1 -element reflexive TopSpace-like TopRelStr;

        set BB = the set of all (( uparrow x) ` ) where x be Element of T;

        reconsider F = {the carrier of T} as Basis of T by YELLOW_9: 10;

        BB c= ( bool the carrier of T)

        proof

          let a be object;

          assume a in BB;

          then ex x be Element of T st a = (( uparrow x) ` );

          hence thesis;

        end;

        then

        reconsider C = BB as Subset-Family of T;

        reconsider C as Subset-Family of T;

        BB = { {} }

        proof

          set x = the Element of T;

          thus BB c= { {} }

          proof

            let a be object;

            assume a in BB;

            then

            consider x be Element of T such that

             A1: a = (( uparrow x) ` );

            x <= x;

            then

             A2: x in ( uparrow x) by WAYBEL_0: 18;

            the carrier of T = {x} by YELLOW_9: 9;

            then a = {} or a = the carrier of T & not x in (( uparrow x) ` ) by A2, A1, XBOOLE_0:def 5, ZFMISC_1: 33;

            hence thesis by TARSKI:def 1, A1;

          end;

          x <= x;

          then

           A3: x in ( uparrow x) by WAYBEL_0: 18;

          the carrier of T = {x} by YELLOW_9: 9;

          then (( uparrow x) ` ) = {} or (( uparrow x) ` ) = the carrier of T & not x in (( uparrow x) ` ) by A3, XBOOLE_0:def 5, ZFMISC_1: 33;

          then {} in BB;

          hence thesis by ZFMISC_1: 31;

        end;

        then ( FinMeetCl C) = { {} , the carrier of T} by YELLOW_9: 11;

        then

         A4: F c= ( FinMeetCl C) by ZFMISC_1: 7;

        BB c= the topology of T

        proof

          let a be object;

          assume a in BB;

          then

          consider x be Element of T such that

           A5: a = (( uparrow x) ` );

          (( uparrow x) ` ) c= {}

          proof

            let y be object;

            x <= x;

            then

             A6: x in ( uparrow x) by WAYBEL_0: 18;

            

             A7: ( uparrow x) misses (( uparrow x) ` ) by XBOOLE_1: 79;

            assume

             A8: y in (( uparrow x) ` );

            then y = x by STRUCT_0:def 10;

            then x in (( uparrow x) /\ (( uparrow x) ` )) by A6, A8, XBOOLE_0:def 4;

            hence thesis by A7;

          end;

          then a = {} by A5;

          hence thesis by PRE_TOPC: 1;

        end;

        hence BB is prebasis of T by A4, CANTOR_1:def 4, TOPS_2: 64;

      end;

    end

    registration

      cluster lower trivial complete strict for TopLattice;

      existence

      proof

        set T = the 1 -element complete strict TopLattice;

        take T;

        thus thesis;

      end;

    end

    theorem :: WAYBEL19:1

    

     Th1: for LL be non empty RelStr holds ex T be strict correct TopAugmentation of LL st T is lower

    proof

      let LL be non empty RelStr;

      set A = the set of all (( uparrow x) ` ) where x be Element of LL;

      A c= ( bool the carrier of LL)

      proof

        let a be object;

        assume a in A;

        then ex x be Element of LL st a = (( uparrow x) ` );

        hence thesis;

      end;

      then

      reconsider A as Subset-Family of LL;

      set T = TopRelStr (# the carrier of LL, the InternalRel of LL, ( UniCl ( FinMeetCl A)) #);

      reconsider S = TopStruct (# the carrier of LL, ( UniCl ( FinMeetCl A)) #) as non empty TopSpace by CANTOR_1: 15;

      

       A1: the TopStruct of T = S;

      T is TopSpace-like by A1, PRE_TOPC:def 1;

      then

      reconsider T as strict non empty TopSpace-like TopRelStr;

      take T;

      set BB = the set of all (( uparrow x) ` ) where x be Element of T;

       the RelStr of T = the RelStr of LL;

      hence T is strict correct TopAugmentation of LL by YELLOW_9:def 4;

      

       A2: A is prebasis of S by CANTOR_1: 18;

      then

      consider F be Basis of S such that

       A3: F c= ( FinMeetCl A) by CANTOR_1:def 4;

      

       A4: the topology of T c= ( UniCl F) by CANTOR_1:def 2;

      F c= the topology of T by TOPS_2: 64;

      then

       A5: F is Basis of T by A4, CANTOR_1:def 2, TOPS_2: 64;

       the RelStr of T = the RelStr of LL;

      then

       A6: A = BB by Lm1;

      A c= the topology of S by A2, TOPS_2: 64;

      hence BB is prebasis of T by A5, A3, A6, CANTOR_1:def 4, TOPS_2: 64;

    end;

    registration

      let R be non empty RelStr;

      cluster lower for strict correct TopAugmentation of R;

      existence by Th1;

    end

    theorem :: WAYBEL19:2

    

     Th2: for L1,L2 be TopSpace-like lower non empty TopRelStr st the RelStr of L1 = the RelStr of L2 holds the topology of L1 = the topology of L2

    proof

      let L1,L2 be TopSpace-like lower non empty TopRelStr such that

       A1: the RelStr of L1 = the RelStr of L2;

      set B2 = the set of all (( uparrow x) ` ) where x be Element of L2;

      set B1 = the set of all (( uparrow x) ` ) where x be Element of L1;

      

       A2: B1 is prebasis of L1 by Def1;

      

       A3: B2 is prebasis of L2 by Def1;

      B1 = B2 by A1, Lm1;

      hence thesis by A1, A2, A3, YELLOW_9: 26;

    end;

    definition

      let R be non empty RelStr;

      :: WAYBEL19:def2

      func omega R -> Subset-Family of R means

      : Def2: for T be lower correct TopAugmentation of R holds it = the topology of T;

      uniqueness

      proof

        set T = the lower correct TopAugmentation of R;

        let X1,X2 be Subset-Family of R;

        assume for T be lower correct TopAugmentation of R holds X1 = the topology of T;

        then X1 = the topology of T;

        hence thesis;

      end;

      existence

      proof

        set S = the lower correct TopAugmentation of R;

        

         A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;

        then

        reconsider X = the topology of S as Subset-Family of R;

        take X;

        let T be lower correct TopAugmentation of R;

         the RelStr of T = the RelStr of R by YELLOW_9:def 4;

        hence thesis by A1, Th2;

      end;

    end

    theorem :: WAYBEL19:3

    

     Th3: for R1,R2 be non empty RelStr st the RelStr of R1 = the RelStr of R2 holds ( omega R1) = ( omega R2)

    proof

      let R1,R2 be non empty RelStr such that

       A1: the RelStr of R1 = the RelStr of R2;

      set S = the lower correct TopAugmentation of R1;

       the RelStr of S = the RelStr of R1 by YELLOW_9:def 4;

      then

       A2: S is TopAugmentation of R2 by A1, YELLOW_9:def 4;

      ( omega R1) = the topology of S by Def2;

      hence thesis by A2, Def2;

    end;

    theorem :: WAYBEL19:4

    

     Th4: for T be lower non empty TopRelStr holds for x be Point of T holds (( uparrow x) ` ) is open & ( uparrow x) is closed

    proof

      let T be lower non empty TopRelStr;

      set BB = the set of all (( uparrow x) ` ) where x be Element of T;

      let x be Point of T;

      reconsider a = x as Element of T;

      BB is prebasis of T by Def1;

      then

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

      

       A2: (( uparrow a) ` ) in BB;

      hence (( uparrow x) ` ) in the topology of T by A1;

      thus (( [#] T) \ ( uparrow x)) in the topology of T by A2, A1;

    end;

    theorem :: WAYBEL19:5

    

     Th5: for T be transitive lower non empty TopRelStr holds for A be Subset of T st A is open holds A is lower

    proof

      let T be transitive lower non empty TopRelStr;

      reconsider BB = the set of all (( uparrow x) ` ) where x be Element of T as prebasis of T by Def1;

      let A be Subset of T such that

       A1: A in the topology of T;

      let x,y be Element of T;

      consider F be Basis of T such that

       A2: F c= ( FinMeetCl BB) by CANTOR_1:def 4;

      the topology of T c= ( UniCl F) by CANTOR_1:def 2;

      then

      consider Y be Subset-Family of T such that

       A3: Y c= F and

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

      assume x in A;

      then

      consider Z be set such that

       A5: x in Z and

       A6: Z in Y by A4, TARSKI:def 4;

      Z in F by A3, A6;

      then

      consider X be Subset-Family of T such that

       A7: X c= BB and X is finite and

       A8: Z = ( Intersect X) by A2, CANTOR_1:def 3;

      assume

       A9: x >= y;

      now

        let Q be set;

        assume

         A10: Q in X;

        then Q in BB by A7;

        then

        consider z be Element of T such that

         A11: Q = (( uparrow z) ` );

        ( uparrow z) misses Q by A11, XBOOLE_1: 79;

        then

         A12: (( uparrow z) /\ Q) = ( {} T);

        x in Q by A5, A8, A10, SETFAM_1: 43;

        then not x in ( uparrow z) by A12, XBOOLE_0:def 4;

        then not x >= z by WAYBEL_0: 18;

        then not y >= z by A9, ORDERS_2: 3;

        then not y in ( uparrow z) by WAYBEL_0: 18;

        hence y in Q by A11, XBOOLE_0:def 5;

      end;

      then y in Z by A8, SETFAM_1: 43;

      hence thesis by A4, A6, TARSKI:def 4;

    end;

    theorem :: WAYBEL19:6

    

     Th6: for T be transitive lower non empty TopRelStr holds for A be Subset of T st A is closed holds A is upper

    proof

      let T be transitive lower non empty TopRelStr;

      let A be Subset of T;

      assume (( [#] T) \ A) in the topology of T;

      then (A ` ) is open;

      then

       A1: (A ` ) is lower by Th5;

      let x,y be Element of T;

      assume that

       A2: x in A and

       A3: x <= y and

       A4: not y in A;

      

       A5: y in (A ` ) by A4, XBOOLE_0:def 5;

       not x in (A ` ) by A2, XBOOLE_0:def 5;

      hence thesis by A5, A1, A3;

    end;

    theorem :: WAYBEL19:7

    

     Th7: for T be non empty TopSpace-like TopRelStr holds T is lower iff { (( uparrow F) ` ) where F be Subset of T : F is finite } is Basis of T

    proof

      let T be non empty TopSpace-like TopRelStr;

      set BB = the set of all (( uparrow x) ` ) where x be Element of T;

      BB c= ( bool the carrier of T)

      proof

        let x be object;

        assume x in BB;

        then ex y be Element of T st x = (( uparrow y) ` );

        hence thesis;

      end;

      then

      reconsider BB as Subset-Family of T;

      reconsider T9 = T as non empty RelStr;

      set A = { (( uparrow F) ` ) where F be Subset of T : F is finite };

      reconsider BB as Subset-Family of T;

      

       A1: A = ( FinMeetCl BB)

      proof

        deffunc F( Element of T9) = ( uparrow $1);

        defpred P[ object, object] means ex x be Element of T st x = $2 & $1 = (( uparrow x) ` );

        hereby

          deffunc F( Element of T9) = ( uparrow $1);

          let a be object;

          assume a in A;

          then

          consider F be Subset of T such that

           A2: a = (( uparrow F) ` ) and

           A3: F is finite;

          set Y = { ( uparrow x) where x be Element of T : x in F };

          Y c= ( bool the carrier of T)

          proof

            let a be object;

            assume a in Y;

            then ex x be Element of T st a = ( uparrow x) & x in F;

            hence thesis;

          end;

          then

          reconsider Y as Subset-Family of T;

          reconsider Y as Subset-Family of T;

          ( uparrow F) = ( union Y) by YELLOW_9: 4;

          then

           A4: a = ( Intersect ( COMPLEMENT Y)) by A2, YELLOW_8: 6;

          reconsider Y9 = Y as Subset-Family of T9;

          

           A5: Y9 = { F(x) where x be Element of T9 : x in F };

          

           A6: ( COMPLEMENT Y9) = { ( F(x) ` ) where x be Element of T9 : x in F } from YELLOW_9:sch 2( A5);

          

           A7: ( COMPLEMENT Y) c= BB

          proof

            let b be object;

            assume b in ( COMPLEMENT Y);

            then ex x be Element of T st b = (( uparrow x) ` ) & x in F by A6;

            hence thesis;

          end;

          deffunc F( Element of T) = (( uparrow $1) ` );

          { F(x) where x be Element of T : x in F } is finite from FRAENKEL:sch 21( A3);

          hence a in ( FinMeetCl BB) by A7, A6, A4, CANTOR_1:def 3;

        end;

        let a be object;

        assume a in ( FinMeetCl BB);

        then

        consider Y be Subset-Family of T such that

         A8: Y c= BB and

         A9: Y is finite and

         A10: a = ( Intersect Y) by CANTOR_1:def 3;

         A11:

        now

          let y be object;

          assume y in Y;

          then y in BB by A8;

          then ex x be Element of T st y = (( uparrow x) ` );

          hence ex b be object st b in the carrier of T & P[y, b];

        end;

        consider f be Function such that

         A12: ( dom f) = Y & ( rng f) c= the carrier of T and

         A13: for y be object st y in Y holds P[y, (f . y)] from FUNCT_1:sch 6( A11);

        reconsider F = ( rng f) as Subset of T by A12;

        

         A14: F is finite by A9, A12, FINSET_1: 8;

        set X = { ( uparrow x) where x be Element of T : x in F };

        X c= ( bool the carrier of T)

        proof

          let a be object;

          assume a in X;

          then ex x be Element of T st a = ( uparrow x) & x in F;

          hence thesis;

        end;

        then

        reconsider X as Subset-Family of T;

        reconsider X as Subset-Family of T;

        reconsider X9 = X as Subset-Family of T9;

        

         A15: X9 = { F(x) where x be Element of T9 : x in F };

        

         A16: ( COMPLEMENT X9) = { ( F(x) ` ) where x be Element of T9 : x in F } from YELLOW_9:sch 2( A15);

        

         A17: ( COMPLEMENT X) = Y

        proof

          hereby

            let a be object;

            assume a in ( COMPLEMENT X);

            then

            consider x be Element of T9 such that

             A18: a = (( uparrow x) ` ) and

             A19: x in F by A16;

            consider y be object such that

             A20: y in Y and

             A21: x = (f . y) by A12, A19, FUNCT_1:def 3;

            ex z be Element of T st z = (f . y) & y = (( uparrow z) ` ) by A13, A20;

            hence a in Y by A18, A20, A21;

          end;

          let a be object;

          assume

           A22: a in Y;

          then

          consider z be Element of T such that

           A23: z = (f . a) and

           A24: a = (( uparrow z) ` ) by A13;

          z in F by A12, A22, A23, FUNCT_1:def 3;

          hence thesis by A16, A24;

        end;

        ( uparrow F) = ( union X) by YELLOW_9: 4;

        then a = (( uparrow F) ` ) by A10, A17, YELLOW_8: 6;

        hence thesis by A14;

      end;

      thus thesis by A1, YELLOW_9: 23;

    end;

    theorem :: WAYBEL19:8

    

     Th8: for S,T be lower complete TopLattice, f be Function of S, T st for X be non empty Subset of S holds f preserves_inf_of X holds f is continuous

    proof

      let S,T be lower complete non empty TopLattice;

      reconsider BB = the set of all (( uparrow x) ` ) where x be Element of T as prebasis of T by Def1;

      let f be Function of S, T such that

       A1: for X be non empty Subset of S holds f preserves_inf_of X;

      now

        let A be Subset of T;

        

         A2: ex_inf_of ((f " (A ` )),S) by YELLOW_0: 17;

        

         A3: ex_inf_of ((A ` ),T) by YELLOW_0: 17;

        

         A4: ex_inf_of ((f .: (f " (A ` ))),T) by YELLOW_0: 17;

        assume A in BB;

        then

        consider x be Element of T such that

         A5: A = (( uparrow x) ` );

        set s = ( inf (f " ( uparrow x)));

        per cases ;

          suppose (f " (A ` )) = ( {} S);

          hence (f " (A ` )) is closed;

        end;

          suppose (f " (A ` )) <> {} ;

          then f preserves_inf_of (f " (A ` )) by A1;

          then

           A6: (f . s) = ( inf (f .: (f " (A ` )))) by A5, A2;

          ( inf (A ` )) = x by A5, WAYBEL_0: 39;

          then

           A7: x <= (f . s) by A6, A3, A4, FUNCT_1: 75, YELLOW_0: 35;

          (f " (A ` )) = ( uparrow s)

          proof

            thus (f " (A ` )) c= ( uparrow s)

            proof

              let a be object;

              assume

               A8: a in (f " (A ` ));

              then

              reconsider a as Element of S;

              s <= a by A5, A8, YELLOW_2: 22;

              hence thesis by WAYBEL_0: 18;

            end;

            let a be object;

            assume

             A9: a in ( uparrow s);

            then

            reconsider a as Element of S;

            f preserves_inf_of {s, a} by A1;

            then

             A10: (f . (s "/\" a)) = ((f . s) "/\" (f . a)) by YELLOW_3: 8;

            s <= a by A9, WAYBEL_0: 18;

            then (f . s) = ((f . s) "/\" (f . a)) by A10, YELLOW_5: 10;

            then (f . s) <= (f . a) by YELLOW_0: 23;

            then x <= (f . a) by A7, ORDERS_2: 3;

            then (f . a) in ( uparrow x) by WAYBEL_0: 18;

            hence thesis by A5, FUNCT_2: 38;

          end;

          hence (f " (A ` )) is closed by Th4;

        end;

      end;

      hence thesis by YELLOW_9: 35;

    end;

    theorem :: WAYBEL19:9

    

     Th9: for S,T be lower complete TopLattice, f be Function of S, T st f is infs-preserving holds f is continuous

    proof

      let S,T be lower complete non empty TopLattice;

      let f be Function of S, T;

      assume f is infs-preserving;

      then for X be non empty Subset of S holds f preserves_inf_of X;

      hence thesis by Th8;

    end;

    theorem :: WAYBEL19:10

    

     Th10: for T be lower complete TopLattice, BB be prebasis of T holds for F be non empty filtered Subset of T st for A be Subset of T st A in BB & ( inf F) in A holds F meets A holds ( inf F) in ( Cl F)

    proof

      let T be lower complete TopLattice, BB be prebasis of T;

      let F be non empty filtered Subset of T such that

       A1: for A be Subset of T st A in BB & ( inf F) in A holds F meets A;

      set N = (F opp+id ), x = ( inf F);

      

       A2: for A be Subset of T st A in BB & x in A holds N is_eventually_in A

      proof

        let A be Subset of T;

        assume that

         A3: A in BB and

         A4: x in A;

        A is open by A3, TOPS_2:def 1;

        then

         A5: A is lower by Th5;

        F meets A by A3, A4, A1;

        then

        consider i be object such that

         A6: i in F and

         A7: i in A by XBOOLE_0: 3;

        reconsider i as Element of N by A6, YELLOW_9: 7;

        take i;

        let j be Element of N;

        

         A8: N is full SubRelStr of (T opp ) by YELLOW_9: 7;

        then

        reconsider a = i, b = j as Element of (T opp ) by YELLOW_0: 58;

        assume i <= j;

        then a <= b by A8, YELLOW_0: 59;

        then

         A9: ( ~ b) <= ( ~ a) by YELLOW_7: 1;

        (N . j) = j by YELLOW_9: 7;

        hence thesis by A9, A7, A5;

      end;

      

       A10: the carrier of N = F by YELLOW_9: 7;

      ( rng ( netmap (N,T))) c= F

      proof

        let x be object;

        assume x in ( rng ( netmap (N,T)));

        then

        consider a be object such that

         A11: a in ( dom ( netmap (N,T))) and

         A12: x = (( netmap (N,T)) . a) by FUNCT_1:def 3;

        reconsider a as Element of N by A11;

        x = (N . a) by A12

        .= a by YELLOW_9: 7;

        hence thesis by A10;

      end;

      hence thesis by A2, YELLOW_9: 39;

    end;

    theorem :: WAYBEL19:11

    

     Th11: for S,T be lower complete TopLattice holds for f be Function of S, T st f is continuous holds f is filtered-infs-preserving

    proof

      let S,T be lower complete TopLattice;

      reconsider BB = the set of all (( uparrow x) ` ) where x be Element of S as prebasis of S by Def1;

      let f be Function of S, T such that

       A1: f is continuous;

      let F be Subset of S such that

       A2: F is non empty filtered and ex_inf_of (F,S);

      for A be Subset of S st A in BB & ( inf F) in A holds F meets A

      proof

        let A be Subset of S;

        assume A in BB;

        then

        consider x be Element of S such that

         A3: A = (( uparrow x) ` );

        assume ( inf F) in A;

        then not ( inf F) >= x by A3, YELLOW_9: 1;

        then not F is_>=_than x by YELLOW_0: 33;

        then

        consider y be Element of S such that

         A4: y in F and

         A5: not y >= x;

        y in A by A3, A5, YELLOW_9: 1;

        hence thesis by A4, XBOOLE_0: 3;

      end;

      then

       A6: ( inf F) in ( Cl F) by A2, Th10;

      

       A7: f is monotone

      proof

        let x,y be Element of S such that

         A8: x <= y;

        (f . x) <= (f . x);

        then (f . x) in ( uparrow (f . x)) by WAYBEL_0: 18;

        then

         A9: x in (f " ( uparrow (f . x))) by FUNCT_2: 38;

        ( uparrow (f . x)) is closed by Th4;

        then (f " ( uparrow (f . x))) is closed by A1;

        then (f " ( uparrow (f . x))) is upper by Th6;

        then y in (f " ( uparrow (f . x))) by A9, A8;

        then (f . y) in ( uparrow (f . x)) by FUNCT_2: 38;

        hence thesis by WAYBEL_0: 18;

      end;

      (f . ( inf F)) is_<=_than (f .: F)

      proof

        let x be Element of T;

        assume x in (f .: F);

        then

        consider a be object such that

         A10: a in the carrier of S and

         A11: a in F and

         A12: x = (f . a) by FUNCT_2: 64;

        reconsider a as Element of S by A10;

        ( inf F) is_<=_than F by YELLOW_0: 33;

        then ( inf F) <= a by A11;

        hence thesis by A7, A12;

      end;

      then

       A13: (f . ( inf F)) <= ( inf (f .: F)) by YELLOW_0: 33;

      thus ex_inf_of ((f .: F),T) by YELLOW_0: 17;

      F c= (f " ( uparrow ( inf (f .: F))))

      proof

        let x be object;

        assume

         A14: x in F;

        then

        reconsider s = x as Element of S;

        (f . s) in (f .: F) by A14, FUNCT_2: 35;

        then ( inf (f .: F)) <= (f . s) by YELLOW_2: 22;

        then (f . s) in ( uparrow ( inf (f .: F))) by WAYBEL_0: 18;

        hence thesis by FUNCT_2: 38;

      end;

      then

       A15: ( Cl F) c= ( Cl (f " ( uparrow ( inf (f .: F))))) by PRE_TOPC: 19;

      ( uparrow ( inf (f .: F))) is closed by Th4;

      then (f " ( uparrow ( inf (f .: F)))) is closed by A1;

      then ( Cl F) c= (f " ( uparrow ( inf (f .: F)))) by A15, PRE_TOPC: 22;

      then (f . ( inf F)) in ( uparrow ( inf (f .: F))) by A6, FUNCT_2: 38;

      then (f . ( inf F)) >= ( inf (f .: F)) by WAYBEL_0: 18;

      hence ( inf (f .: F)) = (f . ( inf F)) by A13, ORDERS_2: 2;

    end;

    theorem :: WAYBEL19:12

    for S,T be lower complete TopLattice holds for f be Function of S, T st f is continuous & for X be finite Subset of S holds f preserves_inf_of X holds f is infs-preserving

    proof

      let S,T be lower complete TopLattice;

      let f be Function of S, T;

      assume f is continuous;

      then f is filtered-infs-preserving by Th11;

      then for F be filtered non empty Subset of S holds f preserves_inf_of F;

      hence thesis by WAYBEL_0: 71;

    end;

    theorem :: WAYBEL19:13

    for T be lower TopSpace-like reflexive transitive non empty TopRelStr holds for x be Point of T holds ( Cl {x}) = ( uparrow x)

    proof

      let T be lower TopSpace-like reflexive transitive non empty TopRelStr;

      let x be Point of T;

      reconsider y = x as Element of T;

      y <= y;

      then x in ( uparrow x) by WAYBEL_0: 18;

      then {x} c= ( uparrow x) by ZFMISC_1: 31;

      hence ( Cl {x}) c= ( uparrow x) by Th4, TOPS_1: 5;

      ( Cl {x}) is upper by Th6;

      then

       A1: ( uparrow ( Cl {x})) c= ( Cl {x}) by WAYBEL_0: 24;

      ( uparrow {x}) c= ( uparrow ( Cl {x})) by PRE_TOPC: 18, YELLOW_3: 7;

      hence thesis by A1;

    end;

    definition

      mode TopPoset is TopSpace-like reflexive transitive antisymmetric TopRelStr;

    end

    registration

      cluster lower -> T_0 for non empty TopPoset;

      coherence

      proof

        let T be non empty TopPoset such that

         A1: T is lower;

        now

          assume not T is empty;

          let x,y be Point of T such that

           A2: x <> y;

          reconsider a = x, b = y as Element of T;

          set Vy = (( uparrow a) ` ), Vx = (( uparrow b) ` );

          a <= a;

          then

           A3: not x in Vy by YELLOW_9: 1;

          b <= b;

          then

           A4: not y in Vx by YELLOW_9: 1;

          

           A5: Vx is open by A1, Th4;

          

           A6: Vy is open by A1, Th4;

          per cases by A2, YELLOW_0:def 3;

            suppose not b <= a;

            then a in Vx by YELLOW_9: 1;

            hence (ex V be Subset of T st V is open & x in V & not y in V) or ex V be Subset of T st V is open & not x in V & y in V by A5, A4;

          end;

            suppose not a <= b;

            then b in Vy by YELLOW_9: 1;

            hence (ex V be Subset of T st V is open & x in V & not y in V) or ex V be Subset of T st V is open & not x in V & y in V by A6, A3;

          end;

        end;

        hence thesis by TSP_1:def 3;

      end;

    end

    registration

      let R be lower-bounded non empty RelStr;

      cluster -> lower-bounded for TopAugmentation of R;

      coherence

      proof

        let T be TopAugmentation of R;

         the RelStr of R = the RelStr of T by YELLOW_9:def 4;

        hence thesis by YELLOW_0: 13;

      end;

    end

    theorem :: WAYBEL19:14

    

     Th14: for S,T be non empty RelStr, s be Element of S, t be Element of T holds (( uparrow [s, t]) ` ) = ( [:(( uparrow s) ` ), the carrier of T:] \/ [:the carrier of S, (( uparrow t) ` ):])

    proof

      let S,T be non empty RelStr, s be Element of S, t be Element of T;

      

      thus (( uparrow [s, t]) ` ) = ( [:the carrier of S, the carrier of T:] \ ( uparrow [s, t])) by YELLOW_3:def 2

      .= ( [:the carrier of S, the carrier of T:] \ [:( uparrow s), ( uparrow t):]) by YELLOW10: 40

      .= ( [:(( uparrow s) ` ), the carrier of T:] \/ [:the carrier of S, (( uparrow t) ` ):]) by ZFMISC_1: 103;

    end;

    theorem :: WAYBEL19:15

    

     Th15: for S,T be lower-bounded non empty Poset holds for S9 be lower correct TopAugmentation of S holds for T9 be lower correct TopAugmentation of T holds ( omega [:S, T:]) = the topology of [:S9, T9 qua non empty TopSpace:]

    proof

      let S,T be lower-bounded non empty Poset;

      set ST = the lower correct TopAugmentation of [:S, T:];

      reconsider BX = the set of all (( uparrow x) ` ) where x be Element of ST as prebasis of ST by Def1;

      let S9 be lower correct TopAugmentation of S;

      reconsider BS = the set of all (( uparrow x) ` ) where x be Element of S9 as prebasis of S9 by Def1;

      let T9 be lower correct TopAugmentation of T;

      set SxT = [:S9, T9 qua non empty TopSpace:];

      set B2 = { [:a, the carrier of T9:] where a be Subset of S9 : a in BS };

      

       A1: the RelStr of T9 = the RelStr of T by YELLOW_9:def 4;

      reconsider BT = the set of all (( uparrow x) ` ) where x be Element of T9 as prebasis of T9 by Def1;

      

       A2: the RelStr of S9 = the RelStr of S by YELLOW_9:def 4;

      then

       A3: the carrier of SxT = [:the carrier of S, the carrier of T:] by A1, BORSUK_1:def 2;

      

       A4: the RelStr of ST = [:S, T:] by YELLOW_9:def 4;

      then

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

      

       A6: BX c= the topology of SxT

      proof

        let z be object;

        

         A7: ( [#] T9) is open;

        assume z in BX;

        then

        consider x be Element of ST such that

         A8: z = (( uparrow x) ` );

        consider s,t be object such that

         A9: s in the carrier of S and

         A10: t in the carrier of T and

         A11: x = [s, t] by A5, ZFMISC_1:def 2;

        reconsider t as Element of T by A10;

        reconsider s as Element of S by A9;

        ( uparrow x) = ( uparrow [s, t]) by A4, A11, WAYBEL_0: 13;

        then

         A12: z = ( [:(( uparrow s) ` ), ( [#] T):] \/ [:( [#] S), (( uparrow t) ` ):]) by A4, A8, Th14;

        reconsider s9 = s as Element of S9 by A2;

        reconsider t9 = t as Element of T9 by A1;

        (( uparrow t9) ` ) in BT;

        then

         A13: (( uparrow t9) ` ) is open by TOPS_2:def 1;

        reconsider A1 = [:(( uparrow s) ` ), ( [#] T):], A2 = [:( [#] S), (( uparrow t) ` ):] as Subset of SxT by A3, YELLOW_3:def 2;

        

         A14: ( [#] S9) is open;

        (( uparrow s9) ` ) in BS;

        then

         A15: (( uparrow s9) ` ) is open by TOPS_2:def 1;

        ( uparrow t) = ( uparrow t9) by A1, WAYBEL_0: 13;

        then

         A16: A2 is open by A13, A14, A2, A1, BORSUK_1: 6;

        ( uparrow s) = ( uparrow s9) by A2, WAYBEL_0: 13;

        then A1 is open by A15, A7, A2, A1, BORSUK_1: 6;

        then (A1 \/ A2) is open by A16;

        hence thesis by A12;

      end;

      set B1 = { [:the carrier of S9, b:] where b be Subset of T9 : b in BT };

      reconsider BB = (B1 \/ B2) as prebasis of SxT by YELLOW_9: 41;

      

       A17: ( UniCl the topology of SxT) = the topology of SxT by CANTOR_1: 6;

      BB c= BX

      proof

        let z be object;

        assume

         A18: z in BB;

        per cases by A18, XBOOLE_0:def 3;

          suppose z in B1;

          then

          consider b be Subset of T9 such that

           A19: z = [:the carrier of S9, b:] and

           A20: b in BT;

          consider t9 be Element of T9 such that

           A21: b = (( uparrow t9) ` ) by A20;

          reconsider t = t9 as Element of T by A1;

          reconsider x = [( Bottom S), t] as Element of ST by A4;

          

           A22: ( uparrow x) = ( uparrow [( Bottom S), t]) by A4, WAYBEL_0: 13;

          ( uparrow ( Bottom S)) = the carrier of S by WAYBEL14: 10;

          then

           A23: (( uparrow ( Bottom S)) ` ) = {} by XBOOLE_1: 37;

          ( uparrow t) = ( uparrow t9) by A1, WAYBEL_0: 13;

          

          then (( uparrow [( Bottom S), t]) ` ) = ( [: {} , the carrier of T:] \/ [:the carrier of S, b:]) by A23, A1, A21, Th14

          .= ( {} \/ [:the carrier of S, b:]) by ZFMISC_1: 90

          .= z by A2, A19;

          hence thesis by A4, A22;

        end;

          suppose z in B2;

          then

          consider a be Subset of S9 such that

           A24: z = [:a, the carrier of T9:] and

           A25: a in BS;

          consider s9 be Element of S9 such that

           A26: a = (( uparrow s9) ` ) by A25;

          reconsider s = s9 as Element of S by A2;

          reconsider x = [s, ( Bottom T)] as Element of ST by A4;

          

           A27: ( uparrow x) = ( uparrow [s, ( Bottom T)]) by A4, WAYBEL_0: 13;

          ( uparrow ( Bottom T)) = the carrier of T by WAYBEL14: 10;

          then

           A28: (( uparrow ( Bottom T)) ` ) = {} by XBOOLE_1: 37;

          ( uparrow s) = ( uparrow s9) by A2, WAYBEL_0: 13;

          

          then (( uparrow [s, ( Bottom T)]) ` ) = ( [:a, the carrier of T:] \/ [:the carrier of S, {} :]) by A28, A2, A26, Th14

          .= ( [:a, the carrier of T:] \/ {} ) by ZFMISC_1: 90

          .= z by A1, A24;

          hence thesis by A4, A27;

        end;

      end;

      then ( FinMeetCl BB) c= ( FinMeetCl BX) by A5, A3, CANTOR_1: 14;

      then

       A29: ( UniCl ( FinMeetCl BB)) c= ( UniCl ( FinMeetCl BX)) by A5, A3, CANTOR_1: 9;

      ( FinMeetCl BB) is Basis of SxT by YELLOW_9: 23;

      then

       A30: the topology of SxT = ( UniCl ( FinMeetCl BB)) by YELLOW_9: 22;

      ( FinMeetCl BX) is Basis of ST by YELLOW_9: 23;

      then

       A31: the topology of ST = ( UniCl ( FinMeetCl BX)) by YELLOW_9: 22;

      ( FinMeetCl the topology of SxT) = the topology of SxT by CANTOR_1: 5;

      then ( FinMeetCl BX) c= the topology of SxT by A6, A5, A3, CANTOR_1: 14;

      then ( UniCl ( FinMeetCl BX)) c= the topology of SxT by A5, A3, A17, CANTOR_1: 9;

      then the topology of ST = the topology of SxT by A31, A30, A29;

      hence thesis by Def2;

    end;

    theorem :: WAYBEL19:16

    for S,T be lower lower-bounded non empty TopPoset holds ( omega [:S, T qua Poset:]) = the topology of [:S, T qua non empty TopSpace:]

    proof

      let S,T be lower lower-bounded non empty TopPoset;

      

       A1: T is TopAugmentation of T by YELLOW_9: 44;

      S is TopAugmentation of S by YELLOW_9: 44;

      hence thesis by A1, Th15;

    end;

    theorem :: WAYBEL19:17

    for T,T2 be lower complete TopLattice st T2 is TopAugmentation of [:T, T qua LATTICE:] holds for f be Function of T2, T st f = ( inf_op T) holds f is continuous

    proof

      let T,T2 be lower complete TopLattice such that

       A1: the RelStr of T2 = the RelStr of [:T, T:];

      let f be Function of T2, T such that

       A2: f = ( inf_op T);

      f is infs-preserving

      proof

        let X be Subset of T2;

        reconsider Y = X as Subset of [:T, T:] by A1;

        assume

         A3: ex_inf_of (X,T2);

        thus ex_inf_of ((f .: X),T) by YELLOW_0: 17;

        

         A4: ( inf_op T) preserves_inf_of Y by WAYBEL_0:def 32;

         ex_inf_of (Y, [:T, T:]) by A3, A1, YELLOW_0: 14;

        hence ( inf (f .: X)) = (f . ( inf X)) by A1, A2, A4, YELLOW_0: 27;

      end;

      hence thesis by Th9;

    end;

    begin

    scheme :: WAYBEL19:sch1

    TopInd { T() -> TopLattice , P[ set] } :

for A be Subset of T() st A is open holds P[A]

      provided

       A1: ex K be prebasis of T() st for A be Subset of T() st A in K holds P[A]

       and

       A2: for F be Subset-Family of T() st for A be Subset of T() st A in F holds P[A] holds P[( union F)]

       and

       A3: for A1,A2 be Subset of T() st P[A1] & P[A2] holds P[(A1 /\ A2)]

       and

       A4: P[( [#] T())];

      consider K be prebasis of T() such that

       A5: for A be Subset of T() st A in K holds P[A] by A1;

      let A be Subset of T();

      assume

       A6: A in the topology of T();

      ( FinMeetCl K) is Basis of T() by YELLOW_9: 23;

      then ( UniCl ( FinMeetCl K)) = the topology of T() by YELLOW_9: 22;

      then

      consider X be Subset-Family of T() such that

       A7: X c= ( FinMeetCl K) and

       A8: A = ( union X) by A6, CANTOR_1:def 1;

      reconsider X as Subset-Family of T();

      now

        defpred Q[ set] means for a be Subset-Family of T() st a = $1 holds P[( Intersect a)];

        let A be Subset of T();

        assume A in X;

        then

        consider Y be Subset-Family of T() such that

         A9: Y c= K and

         A10: Y is finite and

         A11: A = ( Intersect Y) by A7, CANTOR_1:def 3;

        

         A12: for x,Z be set st x in Y & Z c= Y & Q[Z] holds Q[(Z \/ {x})]

        proof

          let x,Z be set;

          assume that

           A13: x in Y and

           A14: Z c= Y and

           A15: Q[Z];

          reconsider xx = {x}, Z9 = Z as Subset-Family of T() by A13, A14, XBOOLE_1: 1, ZFMISC_1: 31;

          reconsider xx, Z9 as Subset-Family of T();

          reconsider xx, Z9 as Subset-Family of T();

          reconsider Ax = x, Ay = ( Intersect Z9) as Subset of T() by A13;

          

           A16: P[Ay] by A15;

          let a be Subset-Family of T();

          assume

           A17: a = (Z \/ {x});

          ( Intersect xx) = Ax by MSSUBFAM: 9;

          then

           A18: ( Intersect a) = (Ax /\ Ay) by A17, MSSUBFAM: 8;

          P[Ax] by A5, A9, A13;

          hence thesis by A18, A3, A16;

        end;

        

         A19: Q[ {} ] by A4, SETFAM_1:def 9;

         Q[Y] from FINSET_1:sch 2( A10, A19, A12);

        hence P[A] by A11;

      end;

      hence thesis by A2, A8;

    end;

    theorem :: WAYBEL19:18

    for L1,L2 be up-complete antisymmetric non empty reflexive RelStr st the RelStr of L1 = the RelStr of L2 & for x be Element of L1 holds ( waybelow x) is directed non empty holds L1 is satisfying_axiom_of_approximation implies L2 is satisfying_axiom_of_approximation

    proof

      let L1,L2 be up-complete antisymmetric non empty reflexive RelStr such that

       A1: the RelStr of L1 = the RelStr of L2 and

       A2: for x be Element of L1 holds ( waybelow x) is directed non empty and

       A3: for x be Element of L1 holds x = ( sup ( waybelow x));

      let x be Element of L2;

      reconsider y = x as Element of L1 by A1;

      

       A4: y = ( sup ( waybelow y)) by A3;

      ( waybelow y) is directed non empty by A2;

      then

       A5: ex_sup_of (( waybelow y),L1) by WAYBEL_0: 75;

      ( waybelow y) = ( waybelow x) by A1, YELLOW12: 13;

      hence thesis by A4, A5, A1, YELLOW_0: 26;

    end;

    registration

      let T be continuous non empty Poset;

      cluster -> continuous for TopAugmentation of T;

      coherence

      proof

        let S be TopAugmentation of T;

         the RelStr of S = the RelStr of T by YELLOW_9:def 4;

        hence thesis by YELLOW12: 15;

      end;

    end

    theorem :: WAYBEL19:19

    

     Th19: for T,S be TopSpace, R be Refinement of T, S holds for W be Subset of R st W in the topology of T or W in the topology of S holds W is open

    proof

      let T,S be TopSpace, R be Refinement of T, S;

      let W be Subset of R;

      (the topology of T \/ the topology of S) is prebasis of R by YELLOW_9:def 6;

      then

       A1: (the topology of T \/ the topology of S) c= the topology of R by TOPS_2: 64;

      assume W in the topology of T or W in the topology of S;

      then W in (the topology of T \/ the topology of S) by XBOOLE_0:def 3;

      hence W in the topology of R by A1;

    end;

    theorem :: WAYBEL19:20

    

     Th20: for T,S be TopSpace, R be Refinement of T, S holds for V be Subset of T, W be Subset of R st W = V holds V is open implies W is open by Th19;

    theorem :: WAYBEL19:21

    

     Th21: for T,S be TopSpace st the carrier of T = the carrier of S holds for R be Refinement of T, S holds for V be Subset of T, W be Subset of R st W = V holds V is closed implies W is closed

    proof

      let T,S be TopSpace such that

       A1: the carrier of T = the carrier of S;

      let R be Refinement of T, S;

      let V be Subset of T, W be Subset of R;

      assume

       A2: W = V;

      assume V is closed;

      then

       A3: (V ` ) is open;

      the carrier of R = (the carrier of T \/ the carrier of S) by YELLOW_9:def 6

      .= the carrier of T by A1;

      then (W ` ) in the topology of T by A3, A2;

      then (W ` ) is open by Th19;

      hence thesis;

    end;

    theorem :: WAYBEL19:22

    

     Th22: for T be non empty TopSpace, K,O be set st K c= O & O c= the topology of T holds (K is Basis of T implies O is Basis of T) & (K is prebasis of T implies O is prebasis of T)

    proof

      let T be non empty TopSpace, K,O be set;

      assume that

       A1: K c= O and

       A2: O c= the topology of T;

      K c= the topology of T by A1, A2;

      then

      reconsider K9 = K, O9 = O as Subset-Family of T by A2, XBOOLE_1: 1;

      reconsider K9, O9 as Subset-Family of T;

      reconsider K9, O9 as Subset-Family of T;

      

       A3: ( UniCl K9) c= ( UniCl O9) by A1, CANTOR_1: 9;

      

       A4: ( UniCl the topology of T) = the topology of T by CANTOR_1: 6;

      then

       A5: ( UniCl O9) c= the topology of T by A2, CANTOR_1: 9;

      hereby

        assume K is Basis of T;

        then ( UniCl K9) = the topology of T by YELLOW_9: 22;

        then ( UniCl O9) = the topology of T by A5, A3;

        hence O is Basis of T by YELLOW_9: 22;

      end;

      ( FinMeetCl the topology of T) = the topology of T by CANTOR_1: 5;

      then ( FinMeetCl O9) c= the topology of T by A2, CANTOR_1: 14;

      then

       A6: ( UniCl ( FinMeetCl O9)) c= the topology of T by A4, CANTOR_1: 9;

      assume K is prebasis of T;

      then ( FinMeetCl K9) is Basis of T by YELLOW_9: 23;

      then

       A7: ( UniCl ( FinMeetCl K9)) = the topology of T by YELLOW_9: 22;

      ( FinMeetCl K9) c= ( FinMeetCl O9) by A1, CANTOR_1: 14;

      then ( UniCl ( FinMeetCl K9)) c= ( UniCl ( FinMeetCl O9)) by CANTOR_1: 9;

      then ( UniCl ( FinMeetCl O9)) = the topology of T by A7, A6;

      then ( FinMeetCl O9) is Basis of T by YELLOW_9: 22;

      hence thesis by YELLOW_9: 23;

    end;

    theorem :: WAYBEL19:23

    

     Th23: for T1,T2 be non empty TopSpace st the carrier of T1 = the carrier of T2 holds for T be Refinement of T1, T2 holds for B1 be prebasis of T1, B2 be prebasis of T2 holds (B1 \/ B2) is prebasis of T

    proof

      let T1,T2 be non empty TopSpace such that

       A1: the carrier of T1 = the carrier of T2;

      let T be Refinement of T1, T2;

      let B1 be prebasis of T1, B2 be prebasis of T2;

      the carrier of T = (the carrier of T1 \/ the carrier of T2) by YELLOW_9:def 6

      .= the carrier of T1 by A1;

      then {the carrier of T1, the carrier of T2} = {the carrier of T} by A1, ENUMSET1: 29;

      then

      reconsider K = ((B1 \/ B2) \/ {the carrier of T}) as prebasis of T by YELLOW_9: 58;

      (B1 \/ B2) c= K by XBOOLE_1: 7;

      then

      reconsider K9 = (B1 \/ B2) as Subset-Family of T by XBOOLE_1: 1;

      K c= ( FinMeetCl K9)

      proof

        let a be object;

        assume a in K;

        then a in K9 & K9 c= ( FinMeetCl K9) or a in {the carrier of T} & the carrier of T in ( FinMeetCl K9) by CANTOR_1: 4, CANTOR_1: 8, XBOOLE_0:def 3;

        hence thesis by TARSKI:def 1;

      end;

      then ( FinMeetCl K) c= ( FinMeetCl ( FinMeetCl K9)) by CANTOR_1: 14;

      then

       A2: ( FinMeetCl K) c= ( FinMeetCl K9) by CANTOR_1: 11;

      ( FinMeetCl K9) c= ( FinMeetCl K) by CANTOR_1: 14, XBOOLE_1: 7;

      then ( FinMeetCl K9) = ( FinMeetCl K) by A2;

      then ( FinMeetCl K9) is Basis of T by YELLOW_9: 23;

      hence thesis by YELLOW_9: 23;

    end;

    theorem :: WAYBEL19:24

    for T1,S1,T2,S2 be non empty TopSpace holds for R1 be Refinement of T1, S1, R2 be Refinement of T2, S2 holds for f be Function of T1, T2, g be Function of S1, S2 holds for h be Function of R1, R2 st h = f & h = g holds f is continuous & g is continuous implies h is continuous

    proof

      let T1,S1,T2,S2 be non empty TopSpace;

      let R1 be Refinement of T1, S1, R2 be Refinement of T2, S2;

      let f be Function of T1, T2, g be Function of S1, S2;

      let h be Function of R1, R2 such that

       A1: h = f and

       A2: h = g;

      

       A3: ( [#] S2) <> {} ;

      reconsider K = (the topology of T2 \/ the topology of S2) as prebasis of R2 by YELLOW_9:def 6;

      

       A4: ( [#] T2) <> {} ;

      assume

       A5: f is continuous;

      assume

       A6: g is continuous;

      now

        let A be Subset of R2;

        assume

         A7: A in K;

        per cases by A7, XBOOLE_0:def 3;

          suppose

           A8: A in the topology of T2;

          then

          reconsider A1 = A as Subset of T2;

          A1 is open by A8;

          then (f " A1) is open by A4, A5, TOPS_2: 43;

          hence (h " A) is open by A1, Th20;

        end;

          suppose

           A9: A in the topology of S2;

          then

          reconsider A1 = A as Subset of S2;

          A1 is open by A9;

          then

           A10: (g " A1) is open by A3, A6, TOPS_2: 43;

          R1 is Refinement of S1, T1 by YELLOW_9: 55;

          hence (h " A) is open by A10, A2, Th20;

        end;

      end;

      hence thesis by YELLOW_9: 36;

    end;

    theorem :: WAYBEL19:25

    

     Th25: for T be non empty TopSpace, K be prebasis of T holds for N be net of T, p be Point of T st for A be Subset of T st p in A & A in K holds N is_eventually_in A holds p in ( Lim N)

    proof

      let T be non empty TopSpace, K be prebasis of T;

      let N be net of T, x be Point of T such that

       A1: for A be Subset of T st x in A & A in K holds N is_eventually_in A;

      now

        defpred P[ object, object] means ex D1 be set st D1 = $1 & for i,j be Element of N st i = $2 & j >= i holds (N . j) in D1;

        let A be a_neighborhood of x;

        

         A2: ( Int A) in the topology of T by PRE_TOPC:def 2;

        ( FinMeetCl K) is Basis of T by YELLOW_9: 23;

        then the topology of T = ( UniCl ( FinMeetCl K)) by YELLOW_9: 22;

        then

        consider Y be Subset-Family of T such that

         A3: Y c= ( FinMeetCl K) and

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

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

        then

        consider y be set such that

         A5: x in y and

         A6: y in Y by A4, TARSKI:def 4;

        consider Z be Subset-Family of T such that

         A7: Z c= K and

         A8: Z is finite and

         A9: y = ( Intersect Z) by A3, A6, CANTOR_1:def 3;

        

         A10: for a be object st a in Z holds ex b be object st b in the carrier of N & P[a, b]

        proof

          let a be object;

          assume

           A11: a in Z;

          then

          reconsider a as Subset of T;

          x in a by A5, A9, A11, SETFAM_1: 43;

          then N is_eventually_in a by A1, A7, A11;

          then

          consider i be Element of N such that

           A12: for j be Element of N st j >= i holds (N . j) in a;

          reconsider i as object;

          take i;

          thus i in the carrier of N;

          take a;

          thus thesis by A12;

        end;

        consider f be Function such that

         A13: ( dom f) = Z & ( rng f) c= the carrier of N and

         A14: for a be object st a in Z holds P[a, (f . a)] from FUNCT_1:sch 6( A10);

        reconsider z = ( rng f) as finite Subset of ( [#] N) by A8, A13, FINSET_1: 8;

        ( [#] N) is directed by WAYBEL_0:def 6;

        then

        consider k be Element of N such that k in ( [#] N) and

         A15: k is_>=_than z by WAYBEL_0: 1;

        thus N is_eventually_in A

        proof

          take k;

          let i be Element of N;

          

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

          assume

           A17: i >= k;

          now

            let a be set;

            assume

             A18: a in Z;

            then

             A19: (f . a) in z by A13, FUNCT_1:def 3;

            then

            reconsider j = (f . a) as Element of N;

            

             A20: j <= k by A15, A19;

             P[a, (f . a)] by A14, A18;

            then

            consider D1 be set such that

             A21: D1 = a & for i,j be Element of N st i = (f . a) & j >= i holds (N . j) in D1;

            thus (N . i) in a by A17, ORDERS_2: 3, A21, A20;

          end;

          then

           A22: (N . i) in y by A9, SETFAM_1: 43;

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

          then (N . i) in ( Int A) by A22, A4;

          hence thesis by A16;

        end;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    theorem :: WAYBEL19:26

    

     Th26: for T be non empty TopSpace holds for N be net of T holds for S be Subset of T st N is_eventually_in S holds ( Lim N) c= ( Cl S)

    proof

      let T be non empty TopSpace, N be net of T, S be Subset of T;

      given i be Element of N such that

       A1: for j be Element of N st j >= i holds (N . j) in S;

      let x be object;

      assume

       A2: x in ( Lim N);

      then

      reconsider x as Element of T;

      now

        let G be a_neighborhood of x;

        N is_eventually_in G by A2, YELLOW_6:def 15;

        then

        consider k be Element of N such that

         A3: for j be Element of N st j >= k holds (N . j) in G;

        ( [#] N) is directed by WAYBEL_0:def 6;

        then

        consider j be Element of N such that j in ( [#] N) and

         A4: j >= i and

         A5: j >= k;

        

         A6: (N . j) in G by A3, A5;

        (N . j) in S by A1, A4;

        hence G meets S by A6, XBOOLE_0: 3;

      end;

      hence thesis by CONNSP_2: 27;

    end;

    theorem :: WAYBEL19:27

    

     Th27: for R be non empty RelStr, X be non empty Subset of R holds the mapping of (X +id ) = ( id X) & the mapping of (X opp+id ) = ( id X)

    proof

      let R be non empty RelStr, X be non empty Subset of R;

       A1:

      now

        let x be object;

        assume x in X;

        then

        reconsider i = x as Element of (X +id ) by YELLOW_9: 6;

        

        thus (the mapping of (X +id ) . x) = ((X +id ) . i)

        .= x by YELLOW_9: 6;

      end;

      the carrier of (X +id ) = X by YELLOW_9: 6;

      then ( dom the mapping of (X +id )) = X by FUNCT_2:def 1;

      hence the mapping of (X +id ) = ( id X) by A1, FUNCT_1: 17;

       A2:

      now

        let x be object;

        assume x in X;

        then

        reconsider i = x as Element of (X opp+id ) by YELLOW_9: 7;

        

        thus (the mapping of (X opp+id ) . x) = ((X opp+id ) . i)

        .= x by YELLOW_9: 7;

      end;

      the carrier of (X opp+id ) = X by YELLOW_9: 7;

      then ( dom the mapping of (X opp+id )) = X by FUNCT_2:def 1;

      hence thesis by A2, FUNCT_1: 17;

    end;

    theorem :: WAYBEL19:28

    

     Th28: for R be reflexive antisymmetric non empty RelStr, x be Element of R holds (( uparrow x) /\ ( downarrow x)) = {x}

    proof

      let R be reflexive antisymmetric non empty RelStr, x be Element of R;

      hereby

        let a be object;

        assume

         A1: a in (( uparrow x) /\ ( downarrow x));

        then

        reconsider y = a as Element of R;

        y in ( downarrow x) by A1, XBOOLE_0:def 4;

        then

         A2: y <= x by WAYBEL_0: 17;

        y in ( uparrow x) by A1, XBOOLE_0:def 4;

        then x <= y by WAYBEL_0: 18;

        then x = a by A2, ORDERS_2: 2;

        hence a in {x} by TARSKI:def 1;

      end;

      

       A3: x <= x;

      then

       A4: x in ( downarrow x) by WAYBEL_0: 17;

      x in ( uparrow x) by A3, WAYBEL_0: 18;

      then x in (( uparrow x) /\ ( downarrow x)) by A4, XBOOLE_0:def 4;

      hence thesis by ZFMISC_1: 31;

    end;

    begin

    definition

      let T be reflexive non empty TopRelStr;

      :: WAYBEL19:def3

      attr T is Lawson means

      : Def3: (( omega T) \/ ( sigma T)) is prebasis of T;

    end

    theorem :: WAYBEL19:29

    

     Th29: for R be complete LATTICE holds for LL be lower correct TopAugmentation of R holds for S be Scott TopAugmentation of R holds for T be correct TopAugmentation of R holds T is Lawson iff T is Refinement of S, LL

    proof

      let R be complete LATTICE;

      let LL be lower correct TopAugmentation of R;

      let S be Scott TopAugmentation of R;

      let T be correct TopAugmentation of R;

      

       A1: the topology of S = ( sigma R) by YELLOW_9: 51;

      

       A2: (the carrier of R \/ the carrier of R) = the carrier of R;

      

       A3: the topology of LL = ( omega R) by Def2;

      

       A4: the RelStr of LL = the RelStr of R by YELLOW_9:def 4;

      

       A5: the RelStr of S = the RelStr of R by YELLOW_9:def 4;

      

       A6: the RelStr of T = the RelStr of R by YELLOW_9:def 4;

      then

       A7: ( sigma T) = ( sigma R) by YELLOW_9: 52;

      ( omega T) = ( omega R) by A6, Th3;

      hence thesis by A7, A3, A1, A2, A4, A5, A6, YELLOW_9:def 6;

    end;

    registration

      let R be complete LATTICE;

      cluster Lawson strict correct for TopAugmentation of R;

      existence

      proof

        set S = the Scott correct TopAugmentation of R;

        set T = the lower correct TopAugmentation of R;

        

         A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;

        set RR = the Refinement of S, T;

        

         A2: the carrier of RR = (the carrier of S \/ the carrier of T) by YELLOW_9:def 6;

        

         A3: the RelStr of T = the RelStr of R by YELLOW_9:def 4;

        then

        reconsider O = the topology of RR as Subset-Family of R by A2, A1;

        set LL = TopRelStr (# the carrier of R, the InternalRel of R, O #);

         the RelStr of LL = the RelStr of R;

        then

        reconsider LL as TopAugmentation of R by YELLOW_9:def 4;

         the TopStruct of LL = the TopStruct of RR by A3, A1, A2;

        then

         A4: LL is correct by TEX_2: 7;

        reconsider A = (the topology of S \/ the topology of T) as prebasis of RR by YELLOW_9:def 6;

        reconsider A9 = A as Subset-Family of LL by A3, A1, A2;

        take LL;

        ( FinMeetCl A) is Basis of RR by YELLOW_9: 23;

        then ( UniCl ( FinMeetCl A)) = O by YELLOW_9: 22;

        then ( FinMeetCl A9) is Basis of LL by A3, A1, A2, A4, YELLOW_9: 22;

        then (the topology of S \/ the topology of T) is prebasis of LL by A4, YELLOW_9: 23;

        then LL is Refinement of S, T by A3, A1, A2, A4, YELLOW_9:def 6;

        hence thesis by Th29;

      end;

    end

    registration

      cluster Scott complete strict for TopLattice;

      existence

      proof

        set R = the complete LATTICE;

        set T = the strict Scott correct TopAugmentation of R;

        take T;

        thus thesis;

      end;

      cluster Lawson continuous for complete strict TopLattice;

      existence

      proof

        set R = the continuous complete LATTICE;

        set T = the strict Lawson correct TopAugmentation of R;

        take T;

        thus thesis;

      end;

    end

    theorem :: WAYBEL19:30

    

     Th30: for T be Lawson complete TopLattice holds (( sigma T) \/ the set of all (( uparrow x) ` ) where x be Element of T) is prebasis of T

    proof

      let T be Lawson complete TopLattice;

      set R = the lower correct TopAugmentation of T;

      set S = the Scott TopAugmentation of T;

      

       A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      T is TopAugmentation of T by YELLOW_9: 44;

      then

       A2: T is Refinement of S, R by Th29;

      set K = the set of all (( uparrow x) ` ) where x be Element of R;

      set O = the set of all (( uparrow x) ` ) where x be Element of T;

      the topology of S = ( sigma T) by YELLOW_9: 51;

      then ( sigma T) is Basis of S by CANTOR_1: 2;

      then

       A3: ( sigma T) is prebasis of S by YELLOW_9: 27;

      

       A4: the RelStr of R = the RelStr of T by YELLOW_9:def 4;

      O = K

      proof

        hereby

          let a be object;

          assume a in O;

          then

          consider x be Element of T such that

           A5: a = (( uparrow x) ` );

          reconsider y = x as Element of R by A4;

          ( uparrow x) = ( uparrow y) by A4, WAYBEL_0: 13;

          hence a in K by A4, A5;

        end;

        let a be object;

        assume a in K;

        then

        consider x be Element of R such that

         A6: a = (( uparrow x) ` );

        reconsider y = x as Element of T by A4;

        ( uparrow x) = ( uparrow y) by A4, WAYBEL_0: 13;

        hence thesis by A4, A6;

      end;

      then

      reconsider O as prebasis of R by Def1;

      O = O;

      hence thesis by A3, A2, A1, A4, Th23;

    end;

    theorem :: WAYBEL19:31

    for T be Lawson complete TopLattice holds (( sigma T) \/ { (W \ ( uparrow x)) where W be Subset of T, x be Element of T : W in ( sigma T) }) is prebasis of T

    proof

      let T be Lawson complete TopLattice;

      set R = the lower correct TopAugmentation of T;

      reconsider K = the set of all (( uparrow x) ` ) where x be Element of R as prebasis of R by Def1;

      set O = { (W \ ( uparrow x)) where W be Subset of T, x be Element of T : W in ( sigma T) };

      O c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in O;

        then ex W be Subset of T, x be Element of T st a = (W \ ( uparrow x)) & W in ( sigma T);

        hence thesis;

      end;

      then

      reconsider O as Subset-Family of T;

      reconsider O as Subset-Family of T;

      set S = the Scott TopAugmentation of T;

      

       A1: the RelStr of R = the RelStr of T by YELLOW_9:def 4;

      (( sigma T) \/ ( omega T)) is prebasis of T by Def3;

      then

       A2: (( sigma T) \/ ( omega T)) c= the topology of T by TOPS_2: 64;

      ( omega T) c= (( sigma T) \/ ( omega T)) by XBOOLE_1: 7;

      then

       A3: ( omega T) c= the topology of T by A2;

      ( sigma T) c= (( sigma T) \/ ( omega T)) by XBOOLE_1: 7;

      then

       A4: ( sigma T) c= the topology of T by A2;

      

       A5: ( omega T) = the topology of R by Def2;

      O c= the topology of T

      proof

        let a be object;

        assume a in O;

        then

        consider W be Subset of T, x be Element of T such that

         A6: a = (W \ ( uparrow x)) and

         A7: W in ( sigma T);

        

         A8: a = (W /\ (( uparrow x) ` )) by A6, SUBSET_1: 13;

        reconsider y = x as Element of R by A1;

        ( uparrow x) = ( uparrow y) by A1, WAYBEL_0: 13;

        then

         A9: (( uparrow x) ` ) in K by A1;

        K c= ( omega T) by A5, TOPS_2: 64;

        then (( uparrow x) ` ) in ( omega T) by A9;

        hence thesis by A4, A3, A7, A8, PRE_TOPC:def 1;

      end;

      then

       A10: (( sigma T) \/ O) c= the topology of T by A4, XBOOLE_1: 8;

      

       A11: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      

       A12: ( sigma T) = the topology of S by YELLOW_9: 51;

      then ( sigma T) is Basis of S by CANTOR_1: 2;

      then

       A13: ( sigma T) is prebasis of S by YELLOW_9: 27;

      

       A14: the carrier of S in ( sigma T) by A12, PRE_TOPC:def 1;

      K c= O

      proof

        let a be object;

        assume a in K;

        then

        consider x be Element of R such that

         A15: a = (( uparrow x) ` );

        reconsider y = x as Element of T by A1;

        a = (( [#] T) \ ( uparrow y)) by A1, A15, WAYBEL_0: 13;

        hence thesis by A11, A14;

      end;

      then

       A16: (( sigma T) \/ K) c= (( sigma T) \/ O) by XBOOLE_1: 9;

      T is TopAugmentation of T by YELLOW_9: 44;

      then T is Refinement of S, R by Th29;

      hence thesis by A13, A1, A11, Th23, A16, A10, Th22;

    end;

    theorem :: WAYBEL19:32

    for T be Lawson complete TopLattice holds { (W \ ( uparrow F)) where W,F be Subset of T : W in ( sigma T) & F is finite } is Basis of T

    proof

      let T be Lawson complete TopLattice;

      set R = the lower correct TopAugmentation of T;

      reconsider B2 = { (( uparrow F) ` ) where F be Subset of R : F is finite } as Basis of R by Th7;

      set Z = { (W \ ( uparrow F)) where W,F be Subset of T : W in ( sigma T) & F is finite };

      set S = the Scott TopAugmentation of T;

      

       A1: the topology of S = ( sigma T) by YELLOW_9: 51;

      then

      reconsider B1 = ( sigma T) as Basis of S by CANTOR_1: 2;

      

       A2: the RelStr of R = the RelStr of T by YELLOW_9:def 4;

      B1 c= Z

      proof

        set F9 = ( {} R);

        reconsider G = F9 as Subset of T by A2;

        let x be object;

        assume

         A3: x in B1;

        then

        reconsider x9 = x as Subset of T;

        ( uparrow G) = ( uparrow F9);

        then (x9 \ ( uparrow G)) = x9;

        hence thesis by A3;

      end;

      then

       A4: (B1 \/ Z) = Z by XBOOLE_1: 12;

      

       A5: ( INTERSECTION (B1,B2)) = Z

      proof

        hereby

          let x be object;

          assume x in ( INTERSECTION (B1,B2));

          then

          consider y,z be set such that

           A6: y in B1 and

           A7: z in B2 and

           A8: x = (y /\ z) by SETFAM_1:def 5;

          reconsider y as Subset of T by A6;

          

           A9: (( [#] T) /\ y) = y by XBOOLE_1: 28;

          consider F be Subset of R such that

           A10: z = (( uparrow F) ` ) and

           A11: F is finite by A7;

          reconsider G = F as Subset of T by A2;

          z = (( uparrow G) ` ) by A2, A10, WAYBEL_0: 13;

          then x = (y \ ( uparrow G)) by A9, A8, XBOOLE_1: 49;

          hence x in Z by A6, A11;

        end;

        let x be object;

        assume x in Z;

        then

        consider W,F be Subset of T such that

         A12: x = (W \ ( uparrow F)) and

         A13: W in ( sigma T) and

         A14: F is finite;

        (W /\ ( [#] T)) = W by XBOOLE_1: 28;

        then

         A15: x = (W /\ (( [#] T) \ ( uparrow F))) by A12, XBOOLE_1: 49;

        reconsider G = F as Subset of R by A2;

        

         A16: (( uparrow G) ` ) in B2 by A14;

        (( uparrow F) ` ) = (( uparrow G) ` ) by A2, WAYBEL_0: 13;

        hence thesis by A16, A13, A15, SETFAM_1:def 5;

      end;

      

       A17: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      B2 c= Z

      proof

        let x be object;

        assume x in B2;

        then

        consider F be Subset of R such that

         A18: x = (( uparrow F) ` ) and

         A19: F is finite;

        

         A20: the carrier of S in B1 by A1, PRE_TOPC:def 1;

        reconsider G = F as Subset of T by A2;

        ( uparrow F) = ( uparrow G) by A2, WAYBEL_0: 13;

        hence thesis by A17, A20, A2, A18, A19;

      end;

      then

       A21: (B2 \/ Z) = Z by XBOOLE_1: 12;

      T is TopAugmentation of T by YELLOW_9: 44;

      then T is Refinement of S, R by Th29;

      then ((B1 \/ B2) \/ ( INTERSECTION (B1,B2))) is Basis of T by YELLOW_9: 59;

      hence thesis by A4, A5, A21, XBOOLE_1: 4;

    end;

    definition

      let T be complete LATTICE;

      :: WAYBEL19:def4

      func lambda T -> Subset-Family of T means

      : Def4: for S be Lawson correct TopAugmentation of T holds it = the topology of S;

      uniqueness

      proof

        set S = the Lawson correct TopAugmentation of T;

        let L1,L2 be Subset-Family of T;

        assume for S be Lawson correct TopAugmentation of T holds L1 = the topology of S;

        then L1 = the topology of S;

        hence thesis;

      end;

      existence

      proof

        set S = the Lawson correct TopAugmentation of T;

        

         A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

        then

        reconsider t = the topology of S as Subset-Family of T;

        take t;

        let S9 be Lawson correct TopAugmentation of T;

        

         A2: the RelStr of S9 = the RelStr of T by YELLOW_9:def 4;

        then

         A3: ( sigma S9) = ( sigma S) by A1, YELLOW_9: 52;

        (( omega S9) \/ ( sigma S9)) is prebasis of S9 by Def3;

        then

         A4: ( FinMeetCl (( omega S9) \/ ( sigma S9))) is Basis of S9 by YELLOW_9: 23;

        

         A5: ( omega S9) = ( omega S) by A2, A1, Th3;

        (( omega S) \/ ( sigma S)) is prebasis of S by Def3;

        then ( FinMeetCl (( omega S) \/ ( sigma S))) is Basis of S by YELLOW_9: 23;

        

        hence t = ( UniCl ( FinMeetCl (( omega S) \/ ( sigma S)))) by YELLOW_9: 22

        .= the topology of S9 by A1, A2, A5, A3, A4, YELLOW_9: 22;

      end;

    end

    theorem :: WAYBEL19:33

    

     Th33: for R be complete LATTICE holds ( lambda R) = ( UniCl ( FinMeetCl (( sigma R) \/ ( omega R))))

    proof

      let R be complete LATTICE;

      set S = the Lawson correct TopAugmentation of R;

      

       A1: the RelStr of S = the RelStr of R by YELLOW_9:def 4;

      then

       A2: ( sigma R) = ( sigma S) by YELLOW_9: 52;

      (( omega S) \/ ( sigma S)) is prebasis of S by Def3;

      then ( FinMeetCl (( omega S) \/ ( sigma S))) is Basis of S by YELLOW_9: 23;

      then

       A3: the topology of S = ( UniCl ( FinMeetCl (( omega S) \/ ( sigma S)))) by YELLOW_9: 22;

      ( omega R) = ( omega S) by A1, Th3;

      hence thesis by A3, A1, A2, Def4;

    end;

    theorem :: WAYBEL19:34

    for R be complete LATTICE holds for T be lower correct TopAugmentation of R holds for S be Scott correct TopAugmentation of R holds for M be Refinement of S, T holds ( lambda R) = the topology of M

    proof

      let R be complete LATTICE;

      let T be lower correct TopAugmentation of R;

      let S be Scott correct TopAugmentation of R;

      let M be Refinement of S, T;

      

       A1: the RelStr of T = the RelStr of R by YELLOW_9:def 4;

      

       A2: (the carrier of R \/ the carrier of R) = the carrier of R;

       the RelStr of S = the RelStr of R by YELLOW_9:def 4;

      then

       A3: the carrier of M = the carrier of R by A2, A1, YELLOW_9:def 6;

      

       A4: ( sigma R) = the topology of S by YELLOW_9: 51;

      ( omega R) = the topology of T by Def2;

      then (( sigma R) \/ ( omega R)) is prebasis of M by A4, YELLOW_9:def 6;

      then

       A5: ( FinMeetCl (( sigma R) \/ ( omega R))) is Basis of M by A3, YELLOW_9: 23;

      

      thus ( lambda R) = ( UniCl ( FinMeetCl (( sigma R) \/ ( omega R)))) by Th33

      .= the topology of M by A3, A5, YELLOW_9: 22;

    end;

    

     Lm2: for T be LATTICE, F be Subset-Family of T st for A be Subset of T st A in F holds A is property(S) holds ( union F) is property(S)

    proof

      let T be LATTICE, F be Subset-Family of T such that

       A1: for A be Subset of T st A in F holds A is property(S);

      let D be non empty directed Subset of T;

      assume ( sup D) in ( union F);

      then

      consider A be set such that

       A2: ( sup D) in A and

       A3: A in F by TARSKI:def 4;

      reconsider A as Subset of T by A3;

      A is property(S) by A1, A3;

      then

      consider y be Element of T such that

       A4: y in D and

       A5: for x be Element of T st x in D & x >= y holds x in A by A2;

      take y;

      thus y in D by A4;

      let x be Element of T;

      assume that

       A6: x in D and

       A7: x >= y;

      x in A by A6, A7, A5;

      hence thesis by A3, TARSKI:def 4;

    end;

    

     Lm3: for T be LATTICE holds for A1,A2 be Subset of T st A1 is property(S) & A2 is property(S) holds (A1 /\ A2) is property(S)

    proof

      let T be LATTICE, A1,A2 be Subset of T such that

       A1: for D be non empty directed Subset of T st ( sup D) in A1 holds ex y be Element of T st y in D & for x be Element of T st x in D & x >= y holds x in A1 and

       A2: for D be non empty directed Subset of T st ( sup D) in A2 holds ex y be Element of T st y in D & for x be Element of T st x in D & x >= y holds x in A2;

      let D be non empty directed Subset of T;

      assume

       A3: ( sup D) in (A1 /\ A2);

      then ( sup D) in A1 by XBOOLE_0:def 4;

      then

      consider y1 be Element of T such that

       A4: y1 in D and

       A5: for x be Element of T st x in D & x >= y1 holds x in A1 by A1;

      ( sup D) in A2 by A3, XBOOLE_0:def 4;

      then

      consider y2 be Element of T such that

       A6: y2 in D and

       A7: for x be Element of T st x in D & x >= y2 holds x in A2 by A2;

      consider y be Element of T such that

       A8: y in D and

       A9: y1 <= y and

       A10: y2 <= y by A4, A6, WAYBEL_0:def 1;

      take y;

      thus y in D by A8;

      let x be Element of T;

      assume that

       A11: x in D and

       A12: x >= y;

      

       A13: x in A2 by A12, A10, A7, A11, ORDERS_2: 3;

      x in A1 by A12, A9, A5, A11, ORDERS_2: 3;

      hence thesis by A13, XBOOLE_0:def 4;

    end;

    

     Lm4: for T be LATTICE holds ( [#] T) is property(S)

    proof

      let T be LATTICE;

      let D be non empty directed Subset of T such that ( sup D) in ( [#] T);

      set y = the Element of D;

      reconsider y as Element of T;

      take y;

      thus thesis;

    end;

    theorem :: WAYBEL19:35

    

     Th35: for T be lower up-complete TopLattice holds for A be Subset of T st A is open holds A is property(S)

    proof

      let T be lower up-complete TopLattice;

      defpred P[ Subset of T] means $1 is property(S);

      

       A1: ex K be prebasis of T st for A be Subset of T st A in K holds P[A]

      proof

        reconsider K = the set of all (( uparrow x) ` ) where x be Element of T as prebasis of T by Def1;

        take K;

        let A be Subset of T;

        assume A in K;

        then

        consider x be Element of T such that

         A2: A = (( uparrow x) ` );

        let D be non empty directed Subset of T;

        assume

         A3: ( sup D) in A;

        set y = the Element of D;

        reconsider y as Element of T;

        take y;

        thus y in D;

        let z be Element of T;

        assume that

         A4: z in D and z >= y and

         A5: not z in A;

        

         A6: z >= x by A5, A2, YELLOW_9: 1;

         not x <= ( sup D) by A3, A2, YELLOW_9: 1;

        then

         A7: not z <= ( sup D) by A6, ORDERS_2: 3;

        

         A8: ex_sup_of (D,T) by WAYBEL_0: 75;

        

         A9: ex_sup_of ( {z},T) by YELLOW_0: 38;

         {z} c= D by A4, ZFMISC_1: 31;

        then ( sup {z}) <= ( sup D) by A8, A9, YELLOW_0: 34;

        hence thesis by A7, YELLOW_0: 39;

      end;

      

       A10: for A1,A2 be Subset of T st P[A1] & P[A2] holds P[(A1 /\ A2)] by Lm3;

      

       A11: P[( [#] T)] by Lm4;

      

       A12: for F be Subset-Family of T st for A be Subset of T st A in F holds P[A] holds P[( union F)] by Lm2;

      thus for A be Subset of T st A is open holds P[A] from TopInd( A1, A12, A10, A11);

    end;

    theorem :: WAYBEL19:36

    

     Th36: for T be Lawson complete TopLattice holds for A be Subset of T st A is open holds A is property(S)

    proof

      let T be Lawson complete TopLattice;

      defpred P[ Subset of T] means $1 is property(S);

      set S = the Scott TopAugmentation of T, R = the lower correct TopAugmentation of T;

      

       A1: the RelStr of R = the RelStr of T by YELLOW_9:def 4;

      

       A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      

       A3: ex K be prebasis of T st for A be Subset of T st A in K holds P[A]

      proof

        reconsider K = (( sigma T) \/ ( omega T)) as prebasis of T by Def3;

        take K;

        let A be Subset of T;

        reconsider AS = A as Subset of S by A2;

        reconsider AR = A as Subset of R by A1;

        assume A in K;

        then A in ( sigma T) & ( sigma T) = the topology of S or A in ( omega T) & ( omega T) = the topology of R by Def2, XBOOLE_0:def 3, YELLOW_9: 51;

        then AS is open or AR is open;

        then AS is property(S) or AR is property(S) by Th35, WAYBEL11: 15;

        hence thesis by A2, A1, YELLOW12: 19;

      end;

      

       A4: P[( [#] T)];

      

       A5: for A1,A2 be Subset of T st P[A1] & P[A2] holds P[(A1 /\ A2)] by Lm3;

      

       A6: for F be Subset-Family of T st for A be Subset of T st A in F holds P[A] holds P[( union F)] by Lm2;

      thus for A be Subset of T st A is open holds P[A] from TopInd( A3, A6, A5, A4);

    end;

    theorem :: WAYBEL19:37

    

     Th37: for S be Scott complete TopLattice holds for T be Lawson correct TopAugmentation of S holds for A be Subset of S st A is open holds for C be Subset of T st C = A holds C is open

    proof

      let S be Scott complete TopLattice;

      let T be Lawson correct TopAugmentation of S;

      let A be Subset of S;

      assume

       A1: A in the topology of S;

      let C be Subset of T;

      assume

       A2: C = A;

      (( sigma T) \/ ( omega T)) is prebasis of T by Def3;

      then

       A3: (( sigma T) \/ ( omega T)) c= the topology of T by TOPS_2: 64;

       the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      then S is Scott TopAugmentation of T by YELLOW_9:def 4;

      then A in ( sigma T) by A1, YELLOW_9: 51;

      then C in (( sigma T) \/ ( omega T)) by A2, XBOOLE_0:def 3;

      hence C in the topology of T by A3;

    end;

    theorem :: WAYBEL19:38

    

     Th38: for T be Lawson complete TopLattice holds for x be Element of T holds ( uparrow x) is closed & ( downarrow x) is closed & {x} is closed

    proof

      let T be Lawson complete TopLattice;

      set S = the Scott TopAugmentation of T;

      set R = the lower correct TopAugmentation of T;

      

       A: the RelStr of S = the RelStr of T & the RelStr of R = the RelStr of T by YELLOW_9:def 4;

      T is TopAugmentation of T by YELLOW_9: 44;

      then

       C: T is Refinement of S, R by Th29;

      then

       D: T is Refinement of R, S by YELLOW_9: 55;

      let x be Element of T;

      reconsider y = x as Element of S by A;

      reconsider z = x as Element of R by A;

      ( downarrow y) = ( downarrow x) & ( downarrow y) is closed & ( uparrow z) = ( uparrow x) & ( uparrow z) is closed by A, WAYBEL_0: 13, Th4, WAYBEL11: 11;

      hence ( uparrow x) is closed & ( downarrow x) is closed by A, C, D, Th21;

      then (( uparrow x) /\ ( downarrow x)) is closed;

      hence thesis by Th28;

    end;

    theorem :: WAYBEL19:39

    

     Th39: for T be Lawson complete TopLattice holds for x be Element of T holds (( uparrow x) ` ) is open & (( downarrow x) ` ) is open & ( {x} ` ) is open

    proof

      let T be Lawson complete TopLattice;

      let x be Element of T;

      

       A1: ( downarrow x) is closed by Th38;

      

       A2: {x} is closed by Th38;

      ( uparrow x) is closed by Th38;

      hence thesis by A1, A2;

    end;

    theorem :: WAYBEL19:40

    

     Th40: for T be Lawson complete continuous TopLattice holds for x be Element of T holds ( wayabove x) is open & (( wayabove x) ` ) is closed

    proof

      let T be Lawson continuous complete TopLattice;

      let x be Element of T;

      set S = the Scott TopAugmentation of T;

      

       A1: T is TopAugmentation of S by YELLOW_9: 45;

      

       A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      then

      reconsider v = x as Element of S;

      ( wayabove v) is open by WAYBEL11: 36;

      hence ( wayabove x) is open by A2, A1, Th37, YELLOW12: 13;

      hence thesis;

    end;

    theorem :: WAYBEL19:41

    for S be Scott complete TopLattice holds for T be Lawson correct TopAugmentation of S holds for A be upper Subset of T st A is open holds for C be Subset of S st C = A holds C is open

    proof

      let S be Scott complete TopLattice;

      let T be Lawson correct TopAugmentation of S;

      let A be upper Subset of T;

      assume

       A1: A is open;

      let C be Subset of S;

      

       A2: the RelStr of T = the RelStr of S by YELLOW_9:def 4;

      assume C = A;

      then C is upper property(S) by A1, Th36, A2, WAYBEL_0: 25, YELLOW12: 19;

      hence thesis by WAYBEL11: 15;

    end;

    theorem :: WAYBEL19:42

    for T be Lawson complete TopLattice holds for A be lower Subset of T holds A is closed iff A is closed_under_directed_sups

    proof

      let T be Lawson complete TopLattice;

      let A be lower Subset of T;

      set S = the Scott TopAugmentation of T;

      hereby

        assume A is closed;

        then (A ` ) is open;

        then

        reconsider mA = (A ` ) as property(S) Subset of T by Th36;

        (mA ` ) = A;

        hence A is directly_closed;

      end;

      assume A is directly_closed;

      then

      reconsider dA = A as directly_closed lower Subset of T;

      

       A1: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      then

      reconsider mA = (dA ` ) as Subset of S;

      mA is upper inaccessible by A1, WAYBEL_0: 25, YELLOW_9: 47;

      then

       A2: mA is open by WAYBEL11:def 4;

      T is TopAugmentation of S by A1, YELLOW_9:def 4;

      then (dA ` ) is open by A2, Th37;

      hence thesis;

    end;

    theorem :: WAYBEL19:43

    for T be Lawson complete TopLattice holds for F be non empty filtered Subset of T holds ( Lim (F opp+id )) = {( inf F)}

    proof

      let T be Lawson complete TopLattice;

      reconsider K = (( sigma T) \/ the set of all (( uparrow x) ` ) where x be Element of T) as prebasis of T by Th30;

      set S = the Scott TopAugmentation of T;

      let F be non empty filtered Subset of T;

      set N = (F opp+id );

      

       A1: the carrier of N = F by YELLOW_9: 7;

      

       A2: N is full SubRelStr of (T opp ) by YELLOW_9: 7;

      thus ( Lim N) c= {( inf F)}

      proof

        let p be object;

        assume

         A3: p in ( Lim N);

        then

        reconsider p as Element of T;

        the mapping of N = ( id F) by Th27;

        then ( rng the mapping of N) = F by RELAT_1: 45;

        then

         A4: p in ( Cl F) by A3, WAYBEL_9: 24;

        p is_<=_than F

        proof

          let u be Element of T;

          assume

           A5: u in F;

          

           A6: N is_eventually_in ( downarrow u)

          proof

            reconsider i = u as Element of N by A5, YELLOW_9: 7;

            take i;

            let j be Element of N;

            j in F by A1;

            then

            reconsider z = j as Element of T;

            assume j >= i;

            then (z ~ ) >= (u ~ ) by A2, YELLOW_0: 59;

            then z <= u by LATTICE3: 9;

            then z in ( downarrow u) by WAYBEL_0: 17;

            hence thesis by YELLOW_9: 7;

          end;

          ( downarrow u) is closed by Th38;

          then ( Cl ( downarrow u)) = ( downarrow u) by PRE_TOPC: 22;

          then ( Lim N) c= ( downarrow u) by A6, Th26;

          hence thesis by A3, WAYBEL_0: 17;

        end;

        then

         A7: p <= ( inf F) by YELLOW_0: 33;

        ( inf F) is_<=_than F by YELLOW_0: 33;

        then

         A8: F c= ( uparrow ( inf F)) by YELLOW_2: 2;

        ( uparrow ( inf F)) is closed by Th38;

        then ( Cl ( uparrow ( inf F))) = ( uparrow ( inf F)) by PRE_TOPC: 22;

        then ( Cl F) c= ( uparrow ( inf F)) by A8, PRE_TOPC: 19;

        then p >= ( inf F) by A4, WAYBEL_0: 18;

        then p = ( inf F) by A7, ORDERS_2: 2;

        hence thesis by TARSKI:def 1;

      end;

      

       A9: the topology of S = ( sigma T) by YELLOW_9: 51;

      

       A10: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

      now

        let A be Subset of T;

        assume that

         A11: ( inf F) in A and

         A12: A in K;

        per cases by A12, XBOOLE_0:def 3;

          suppose

           A13: A in ( sigma T);

          then

          reconsider a = A as Subset of S by A9;

          set i = the Element of N;

          a is open by A9, A13;

          then a is upper by WAYBEL11:def 4;

          then

           A14: A is upper by A10, WAYBEL_0: 25;

          thus N is_eventually_in A

          proof

            take i;

            let j be Element of N;

            j in F by A1;

            then

            reconsider z = j as Element of T;

            z >= ( inf F) by A1, YELLOW_2: 22;

            then z in A by A11, A14;

            hence thesis by YELLOW_9: 7;

          end;

        end;

          suppose A in the set of all (( uparrow x) ` ) where x be Element of T;

          then

          consider x be Element of T such that

           A15: A = (( uparrow x) ` );

           not ( inf F) >= x by A11, A15, YELLOW_9: 1;

          then not F is_>=_than x by YELLOW_0: 33;

          then

          consider y be Element of T such that

           A16: y in F and

           A17: not y >= x;

          thus N is_eventually_in A

          proof

            reconsider i = y as Element of N by A16, YELLOW_9: 7;

            take i;

            let j be Element of N;

            j in F by A1;

            then

            reconsider z = j as Element of T;

            assume j >= i;

            then (z ~ ) >= (y ~ ) by A2, YELLOW_0: 59;

            then z <= y by LATTICE3: 9;

            then not z >= x by A17, ORDERS_2: 3;

            then z in A by A15, YELLOW_9: 1;

            hence thesis by YELLOW_9: 7;

          end;

        end;

      end;

      then ( inf F) in ( Lim N) by Th25;

      hence thesis by ZFMISC_1: 31;

    end;

    registration

      cluster Lawson -> T_1 compact for complete TopLattice;

      coherence

      proof

        let T be complete TopLattice such that

         A1: T is Lawson;

        for x be Point of T holds {x} is closed by A1, Th38;

        hence T is T_1 by URYSOHN1: 19;

        set O1 = ( sigma T), O2 = the set of all (( uparrow x) ` ) where x be Element of T;

        reconsider K = (O1 \/ O2) as prebasis of T by A1, Th30;

        set S = the Scott TopAugmentation of T;

        the carrier of ( InclPoset the topology of T) = the topology of T by YELLOW_1: 1;

        then

        reconsider X = the carrier of T as Element of ( InclPoset the topology of T) by PRE_TOPC:def 1;

        

         A2: the RelStr of S = the RelStr of T by YELLOW_9:def 4;

        for F be Subset of K st X c= ( union F) holds ex G be finite Subset of F st X c= ( union G)

        proof

          deffunc F( Element of T) = (( uparrow $1) ` );

          let F be Subset of K;

          set I2 = { x where x be Element of T : (( uparrow x) ` ) in F };

          set x = ( "\/" (I2,T));

          

           A3: I2 c= the carrier of T

          proof

            let a be object;

            assume a in I2;

            then ex x be Element of T st a = x & (( uparrow x) ` ) in F;

            hence thesis;

          end;

          reconsider z = x as Element of S by A2;

          assume

           A4: X c= ( union F);

          x in X;

          then

          consider Y be set such that

           A5: x in Y and

           A6: Y in F by A4, TARSKI:def 4;

          Y in K by A6;

          then

          reconsider I2, Y as Subset of T by A3;

          reconsider Z = Y, J2 = I2 as Subset of S by A2;

          now

            assume not Y in O1;

            then Y in O2 by A6, XBOOLE_0:def 3;

            then

            consider y be Element of T such that

             A7: Y = (( uparrow y) ` );

            y in I2 by A6, A7;

            then y <= x by YELLOW_2: 22;

            hence contradiction by A5, A7, YELLOW_9: 1;

          end;

          then Z in the topology of S by YELLOW_9: 51;

          then

           A8: Z is open;

          then

           A9: Z is upper by WAYBEL11: 15;

          

           A10: z = ( sup J2) by A2, YELLOW_0: 17, YELLOW_0: 26

          .= ( sup ( finsups J2)) by WAYBEL_0: 55;

          Z is property(S) by A8, WAYBEL11: 15;

          then

          consider y be Element of S such that

           A11: y in ( finsups J2) and

           A12: for x be Element of S st x in ( finsups J2) & x >= y holds x in Z by A10, A5;

          consider a be finite Subset of J2 such that

           A13: y = ( "\/" (a,S)) and ex_sup_of (a,S) by A11;

          set AA = { (( uparrow c) ` ) where c be Element of T : c in a }, G = ( {Y} \/ AA);

          

           A14: G c= F

          proof

            let i be object;

            assume that

             A15: i in G and

             A16: not i in F;

            i in {Y} or i in AA by A15, XBOOLE_0:def 3;

            then

            consider c be Element of T such that

             A17: i = (( uparrow c) ` ) and

             A18: c in a by A6, A16, TARSKI:def 1;

            c in J2 by A18;

            then ex c9 be Element of T st c = c9 & (( uparrow c9) ` ) in F;

            hence contradiction by A16, A17;

          end;

          

           A19: a is finite;

          { F(c) where c be Element of T : c in a } is finite from FRAENKEL:sch 21( A19);

          then

          reconsider G as finite Subset of F by A14;

          take G;

          let u be object;

          assume that

           A20: u in X and

           A21: not u in ( union G);

          reconsider u as Element of S by A20, A2;

          

           A22: ( union G) = (( union {Y}) \/ ( union AA)) by ZFMISC_1: 78

          .= (Y \/ ( union AA)) by ZFMISC_1: 25;

          then

           A23: not u in Y by A21, XBOOLE_0:def 3;

          

           A24: not u in ( union AA) by A22, A21, XBOOLE_0:def 3;

          

           A25: y <= y & u is_>=_than a

          proof

            thus y <= y;

            let v be Element of S;

            assume

             A26: v in a;

            then v in J2;

            then

            consider c be Element of T such that

             A27: v = c and (( uparrow c) ` ) in F;

            (( uparrow c) ` ) in AA by A26, A27;

            then

             A28: not u in (( uparrow c) ` ) by A24, TARSKI:def 4;

            (( uparrow c) ` ) = (( uparrow v) ` ) by A2, A27, WAYBEL_0: 13;

            hence thesis by A28, YELLOW_9: 1;

          end;

          then

           A29: u >= y by A13, YELLOW_0: 32;

          y in Z by A25, A11, A12;

          hence thesis by A29, A9, A23;

        end;

        then X << X by WAYBEL_7: 31;

        then X is compact;

        hence thesis by WAYBEL_3: 37;

      end;

    end

    registration

      cluster Lawson -> Hausdorff for complete continuous TopLattice;

      coherence

      proof

        let T be complete continuous TopLattice such that

         A1: T is Lawson;

        let x,y be Point of T such that

         A2: x <> y;

        reconsider x9 = x, y9 = y as Element of T;

        

         A3: for x be Element of T holds ( waybelow x) is non empty directed;

        per cases by A2, ORDERS_2: 2;

          suppose not y9 <= x9;

          then

          consider u be Element of T such that

           A4: u << y9 and

           A5: not u <= x9 by A3, WAYBEL_3: 24;

          take V = (( uparrow u) ` ), W = ( wayabove u);

          thus V is open & W is open by A1, Th39, Th40;

          thus x in V by A5, YELLOW_9: 1;

          thus y in W by A4;

          

           A6: (V ` ) = ( uparrow u);

          W c= ( uparrow u) by WAYBEL_3: 11;

          hence thesis by A6, SUBSET_1: 23;

        end;

          suppose not x9 <= y9;

          then

          consider u be Element of T such that

           A7: u << x9 and

           A8: not u <= y9 by A3, WAYBEL_3: 24;

          take W = ( wayabove u), V = (( uparrow u) ` );

          thus W is open & V is open by A1, Th39, Th40;

          thus x in W by A7;

          thus y in V by A8, YELLOW_9: 1;

          

           A9: (V ` ) = ( uparrow u);

          W c= ( uparrow u) by WAYBEL_3: 11;

          hence thesis by A9, SUBSET_1: 23;

        end;

      end;

    end