waybel32.miz

    begin

    definition

      let T be non empty TopRelStr;

      :: WAYBEL32:def1

      attr T is upper means

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

    end

    registration

      cluster Scott up-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;

    end

    definition

      let T be TopSpace-like non empty reflexive TopRelStr;

      :: WAYBEL32:def2

      attr T is order_consistent means

      : Def2: for x be Element of T holds ( downarrow x) = ( Cl {x}) & for N be eventually-directed net of T st x = ( sup N) holds for V be a_neighborhood of x holds N is_eventually_in V;

    end

    registration

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

      coherence

      proof

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

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

        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 = (( downarrow x) ` );

          hence thesis;

        end;

        then

        reconsider C = BB as Subset-Family of T;

        reconsider C as Subset-Family of T;



         A1: BB c= the topology of T

        proof

          let a be object;

          reconsider aa = a as set by TARSKI: 1;

          assume a in BB;

          then

          consider x be Element of T such that

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

          aa c= {}

          proof

            let y be object;

            assume

             A3: y in aa;



             A4: x <= x;



             A5: y = x by A2, A3, STRUCT_0:def 10;

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

            then

             A6: x in (( downarrow x) /\ aa) by A3, A5, XBOOLE_0:def 4;

            ( downarrow x) misses aa by A2, XBOOLE_1: 79;

            hence thesis by A6;

          end;

          then a = {} ;

          hence thesis by PRE_TOPC: 1;

        end;

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

        BB = { {} }

        proof

          thus BB c= { {} }

          proof

            let a be object;

            reconsider aa = a as set by TARSKI: 1;

            assume a in BB;

            then

            consider x be Element of T such that

             A7: a = (( downarrow x) ` );



             A8: x <= x;



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

            x in ( downarrow x) by A8, WAYBEL_0: 17;

            then a = {} or a = the carrier of T & not x in aa by A7, A9, XBOOLE_0:def 5, ZFMISC_1: 33;

            hence thesis by TARSKI:def 1;

          end;

          set x = the Element of T;



           A10: x <= x;



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

          x in ( downarrow x) by A10, WAYBEL_0: 17;

          then (( downarrow x) ` ) = {} or (( downarrow x) ` ) = the carrier of T & not x in (( downarrow x) ` ) by A11, 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 F c= ( FinMeetCl C) by ZFMISC_1: 7;

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

      end;

    end

    registration

      cluster upper trivial up-complete strict for TopLattice;

      existence

      proof

        set T = the 1 -element up-complete strict TopLattice;

        take T;

        thus thesis;

      end;

    end

    theorem :: WAYBEL32:1



     Th1: for T be upper up-complete non empty TopPoset holds for A be Subset of T st A is open holds A is upper

    proof

      let T be upper up-complete non empty TopPoset;

      let A be Subset of T;

      assume A is open;

      then

       A1: A in the topology of T by PRE_TOPC:def 2;

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

      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;

      let x,y be Element of T;

      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 = (( downarrow z) ` );



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

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

        then not x in ( downarrow z) by A12, XBOOLE_0: 3;

        then not x <= z by WAYBEL_0: 17;

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

        then not y in ( downarrow z) by WAYBEL_0: 17;

        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 :: WAYBEL32:2

    for T be up-complete non empty TopPoset holds T is upper implies T is order_consistent

    proof

      let T be up-complete non empty TopPoset;

      assume

       A1: T is upper;

      then

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

      for x be Element of T holds ( downarrow x) = ( Cl {x}) & for N be eventually-directed net of T st x = ( sup N) holds for V be a_neighborhood of x holds N is_eventually_in V

      proof

        let x be Element of T;



         A2: ( downarrow x) c= ( Cl {x})

        proof

          let a be object;

          assume

           A3: a in ( downarrow x);

          then

          reconsider a9 = a as Point of T;

          for G be Subset of T st G is open holds a9 in G implies {x} meets G

          proof

            let G be Subset of T such that

             A4: G is open;

            assume

             A5: a9 in G;

            reconsider v = a9 as Element of T;



             A6: v <= x by A3, WAYBEL_0: 17;

            G is upper by A1, A4, Th1;

            then

             A7: x in G by A5, A6;

            x in {x} by TARSKI:def 1;

            hence thesis by A7, XBOOLE_0: 3;

          end;

          hence thesis by PRE_TOPC: 24;

        end;

        ( Cl {x}) c= ( downarrow x)

        proof

          let a be object;

          assume

           A8: a in ( Cl {x});

          reconsider BB as Subset-Family of T;

          (( downarrow x) ` ) in BB;

          then

           A9: (( downarrow x) ` ) is open by TOPS_2:def 1;

          (( downarrow x) ` ) = (( [#] T) \ ( downarrow x));

          then

           A10: ( downarrow x) is closed by A9, PRE_TOPC:def 3;

          x <= x;

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

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

          hence thesis by A8, A10, PRE_TOPC: 15;

        end;

        hence ( downarrow x) = ( Cl {x}) by A2;

        thus for N be eventually-directed net of T st x = ( sup N) holds for V be a_neighborhood of x holds N is_eventually_in V

        proof

          let N be eventually-directed net of T;

          assume x = ( sup N);



          then

           A11: x = ( Sup the mapping of N) by WAYBEL_2:def 1

          .= ( sup ( rng ( netmap (N,T)))) by YELLOW_2:def 5;

          let V be a_neighborhood of x;



           A12: x in ( Int V) by CONNSP_2:def 1;

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

          then

           A13: the topology of T = ( UniCl ( FinMeetCl BB)) by YELLOW_9: 22;

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

          then

          consider Y be Subset-Family of T such that

           A14: Y c= ( FinMeetCl BB) and

           A15: ( Int V) = ( union Y) by A13, CANTOR_1:def 1;

          consider Y1 be set such that

           A16: x in Y1 and

           A17: Y1 in Y by A12, A15, TARSKI:def 4;

          consider Z be Subset-Family of T such that

           A18: Z c= BB and

           A19: Z is finite and

           A20: Y1 = ( Intersect Z) by A14, A17, CANTOR_1:def 3;

          reconsider rngN = ( rng ( netmap (N,T))) as Subset of T;

          rngN is directed by WAYBEL_2: 18;

          then ex a be Element of T st a is_>=_than rngN & for b be Element of T st b is_>=_than rngN holds a <= b by WAYBEL_0:def 39;

          then

           A21: ex_sup_of (rngN,T) by YELLOW_0: 15;

          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;



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

          proof

            let Q be object;

            assume

             A23: Q in Z;

            then Q in BB by A18;

            then

            consider v1 be Element of T such that

             A24: Q = (( downarrow v1) ` );

            x in (( downarrow v1) ` ) by A16, A20, A23, A24, SETFAM_1: 43;

            then not x in ( downarrow v1) by XBOOLE_0:def 5;

            then

             A25: not x <= v1 by WAYBEL_0: 17;

             not rngN c= ( downarrow v1)

            proof

              assume

               A26: rngN c= ( downarrow v1);

               ex_sup_of (( downarrow v1),T) by WAYBEL_0: 34;

              then ( sup rngN) <= ( sup ( downarrow v1)) by A21, A26, YELLOW_0: 34;

              hence contradiction by A11, A25, WAYBEL_0: 34;

            end;

            then

            consider w be object such that

             A27: w in rngN and

             A28: not w in ( downarrow v1);

            reconsider w9 = w as Element of T by A27;

            consider i be object such that

             A29: i in ( dom the mapping of N) and

             A30: w9 = (the mapping of N . i) by A27, FUNCT_1:def 3;

            reconsider i as Element of N by A29;

            consider b be Element of N such that

             A31: for l be Element of N st b <= l holds (N . i) <= (N . l) by WAYBEL_0: 11;

            take b;

            thus b in the carrier of N;

            reconsider QQ = Q as set by TARSKI: 1;

            take QQ;

            thus QQ = Q;

            thus for j,k be Element of N st j = b & k >= j holds (N . k) in QQ

            proof

              let j,k be Element of N such that

               A32: j = b and

               A33: k >= j;



               A34: (N . i) <= (N . k) by A31, A32, A33;

               not (N . i) <= v1 by A28, A30, WAYBEL_0: 17;

              then not (N . k) <= v1 by A34, ORDERS_2: 3;

              then not (N . k) in ( downarrow v1) by WAYBEL_0: 17;

              hence thesis by A24, XBOOLE_0:def 5;

            end;

          end;

          consider f be Function such that

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

           A36: for Q be object st Q in Z holds P[Q, (f . Q)] from FUNCT_1:sch 6( A22);

          reconsider rngf = ( rng f) as finite Subset of ( [#] N) by A19, A35, FINSET_1: 8;

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

          then

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

           A37: k is_>=_than rngf by WAYBEL_0: 1;

          take k;

          let k1 be Element of N such that

           A38: k <= k1;

          now

            let Q be set;

            assume

             A39: Q in Z;

            then

             A40: (f . Q) in rngf by A35, FUNCT_1:def 3;

            then

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



             A41: j <= k by A37, A40;

             P[Q, (f . Q)] by A36, A39;

            hence (N . k1) in Q by A38, ORDERS_2: 3, A41;

          end;

          then

           A42: (N . k1) in Y1 by A20, SETFAM_1: 43;

          Y1 c= ( union Y) by A17, ZFMISC_1: 74;

          then

           A43: (N . k1) in ( Int V) by A15, A42;

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

          hence thesis by A43;

        end;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL32:3



     Th3: for R be up-complete non empty reflexive transitive antisymmetric RelStr holds ex T be TopAugmentation of R st T is Scott

    proof

      let R be up-complete non empty reflexive transitive antisymmetric RelStr;

      set T = the Scott TopAugmentation of R;

      take T;

      thus thesis;

    end;

    theorem :: WAYBEL32:4

    for R be up-complete non empty Poset holds for T be TopAugmentation of R holds T is Scott implies T is correct;

    registration

      let R be up-complete non empty reflexive transitive antisymmetric RelStr;

      cluster Scott -> correct for TopAugmentation of R;

      coherence ;

    end

    registration

      let R be up-complete non empty reflexive transitive antisymmetric RelStr;

      cluster Scott correct for TopAugmentation of R;

      existence

      proof

        consider T be TopAugmentation of R such that

         A1: T is Scott by Th3;

        take T;

        thus thesis by A1;

      end;

    end

    theorem :: WAYBEL32:5



     Th5: for T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, x be Element of T holds ( Cl {x}) = ( downarrow x)

    proof

      let T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, x be Element of T;

      reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9: 44;

      reconsider dx = ( downarrow x) as Subset of T9;

      reconsider A = {x} as Subset of T9;



       A1: ( downarrow x) is closed by WAYBEL11: 11;

      x <= x;

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

      then

       A2: {x} c= ( downarrow x) by ZFMISC_1: 31;

      now

        let C be Subset of T9 such that

         A3: A c= C;

        reconsider D = C as Subset of T9;

        assume C is closed;

        then

         A4: D is lower by WAYBEL11: 7;

        x in C by A3, ZFMISC_1: 31;

        hence dx c= C by A4, WAYBEL11: 6;

      end;

      hence thesis by A1, A2, YELLOW_8: 8;

    end;

    theorem :: WAYBEL32:6



     Th6: for T be up-complete Scott non empty TopPoset holds T is order_consistent

    proof

      let T be up-complete Scott non empty TopPoset;

      for x be Element of T holds ( downarrow x) = ( Cl {x}) & for N be eventually-directed net of T st x = ( sup N) holds for V be a_neighborhood of x holds N is_eventually_in V

      proof

        let x be Element of T;

        for N be eventually-directed net of T st x = ( sup N) holds for V be a_neighborhood of x holds N is_eventually_in V

        proof

          let N be eventually-directed net of T;

          assume x = ( sup N);

          then x = ( Sup the mapping of N) by WAYBEL_2:def 1;

          then

           A1: x = ( sup ( rng the mapping of N)) by YELLOW_2:def 5;

          let V be a_neighborhood of x;



           A2: x in ( Int V) by CONNSP_2:def 1;

          reconsider rngN = ( rng ( netmap (N,T))) as Subset of T;

          rngN is directed by WAYBEL_2: 18;

          then ( Int V) meets rngN by A1, A2, WAYBEL11:def 1;

          then

          consider z be object such that

           A3: z in ( Int V) and

           A4: z in rngN by XBOOLE_0: 3;

          reconsider z9 = z as Element of T by A3;

          consider i be object such that

           A5: i in ( dom the mapping of N) and

           A6: z9 = (the mapping of N . i) by A4, FUNCT_1:def 3;

          reconsider i as Element of N by A5;

          consider j be Element of N such that

           A7: for k be Element of N st j <= k holds (N . i) <= (N . k) by WAYBEL_0: 11;

          take j;

          let l be Element of N;

          assume j <= l;

          then (N . i) <= (N . l) by A7;

          then

           A8: (N . l) in ( Int V) by A3, A6, WAYBEL_0:def 20;

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

          hence thesis by A8;

        end;

        hence thesis by Th5;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL32:7



     Th7: for R be /\-complete Semilattice, Z be net of R, D be Subset of R st D = the set of all ( "/\" ({ (Z . k) where k be Element of Z : k >= j },R)) where j be Element of Z holds D is non empty directed

    proof

      let R be /\-complete Semilattice, Z be net of R, D be Subset of R;

      assume

       A1: D = the set of all ( "/\" ({ (Z . k) where k be Element of Z : k >= j },R)) where j be Element of Z;

      set j = the Element of Z;

      ( "/\" ({ (Z . k) where k be Element of Z : k >= j },R)) in D by A1;

      hence D is non empty;

      let x,y be Element of R;

      assume x in D;

      then

      consider jx be Element of Z such that

       A2: x = ( "/\" ({ (Z . k) where k be Element of Z : k >= jx },R)) by A1;

      assume y in D;

      then

      consider jy be Element of Z such that

       A3: y = ( "/\" ({ (Z . k) where k be Element of Z : k >= jy },R)) by A1;

      reconsider jx, jy as Element of Z;

      consider j be Element of Z such that

       A4: j >= jx and

       A5: j >= jy by YELLOW_6:def 3;

      consider j9 be Element of Z such that

       A6: j9 >= j and j9 >= j by YELLOW_6:def 3;

      deffunc F( Element of Z) = (Z . $1);

      defpred Px[ Element of Z] means $1 >= jx;

      defpred Py[ Element of Z] means $1 >= jy;

      defpred P[ Element of Z] means $1 >= j;

      set Ex = { F(k) where k be Element of Z : Px[k] }, Ey = { F(k) where k be Element of Z : Py[k] }, E = { F(k) where k be Element of Z : P[k] };



       A7: (Z . j) in Ex by A4;



       A8: (Z . j) in Ey by A5;



       A9: (Z . j9) in E by A6;



       A10: Ex is Subset of R from DOMAIN_1:sch 8;



       A11: Ey is Subset of R from DOMAIN_1:sch 8;



       A12: E is Subset of R from DOMAIN_1:sch 8;

      take z = ( "/\" ({ (Z . k) where k be Element of Z : k >= j },R));

      reconsider Ex9 = Ex as non empty Subset of R by A7, A10;

      reconsider Ey9 = Ey as non empty Subset of R by A8, A11;

      reconsider E9 = E as non empty Subset of R by A9, A12;



       A13: ex_inf_of (E9,R) by WAYBEL_0: 76;



       A14: ex_inf_of (Ex9,R) by WAYBEL_0: 76;



       A15: ex_inf_of (Ey9,R) by WAYBEL_0: 76;

      thus z in D by A1;

      E9 c= Ex9

      proof

        let e be object;

        assume e in E9;

        then

        consider k be Element of Z such that

         A16: e = (Z . k) and

         A17: k >= j;

        reconsider k as Element of Z;

        k >= jx by A4, A17, YELLOW_0:def 2;

        hence thesis by A16;

      end;

      hence x <= z by A2, A13, A14, YELLOW_0: 35;

      E9 c= Ey9

      proof

        let e be object;

        assume e in E9;

        then

        consider k be Element of Z such that

         A18: e = (Z . k) and

         A19: k >= j;

        reconsider k as Element of Z;

        k >= jy by A5, A19, YELLOW_0:def 2;

        hence thesis by A18;

      end;

      hence y <= z by A3, A13, A15, YELLOW_0: 35;

    end;

    theorem :: WAYBEL32:8



     Th8: for R be /\-complete Semilattice, S be Subset of R, a be Element of R holds a in S implies ( "/\" (S,R)) <= a

    proof

      let R be /\-complete Semilattice, S be Subset of R;

      let a be Element of R;

      assume

       A1: a in S;

      then ex_inf_of (S,R) by WAYBEL_0: 76;

      then S is_>=_than ( "/\" (S,R)) by YELLOW_0: 31;

      hence thesis by A1;

    end;

    theorem :: WAYBEL32:9



     Th9: for R be /\-complete Semilattice, N be monotone reflexive net of R holds ( lim_inf N) = ( sup N)

    proof

      let R be /\-complete Semilattice, N be monotone reflexive net of R;

      deffunc F( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

      deffunc G( Element of N) = (N . $1);

      defpred P[ set] means not contradiction;

      set X = { F(j) where j be Element of N : P[j] };



       A1: for j be Element of N holds G(j) = F(j)

      proof

        let j be Element of N;

        defpred P[ Element of N] means $1 >= j;

        set Y = { G(i) where i be Element of N : P[i] };

        j <= j;

        then

         A2: (N . j) in Y;

        Y is Subset of R from DOMAIN_1:sch 8;

        then

         A3: ex_inf_of (Y,R) by A2, WAYBEL_0: 76;



         A4: (N . j) is_<=_than Y

        proof

          let y be Element of R;

          assume y in Y;

          then ex i be Element of N st y = (N . i) & j <= i;

          hence (N . j) <= y by WAYBEL11:def 9;

        end;

        for b be Element of R st b is_<=_than Y holds (N . j) >= b

        proof

          let b be Element of R;

          assume

           A5: b is_<=_than Y;

          reconsider j9 = j as Element of N;

          j9 <= j9;

          then (N . j9) in Y;

          hence thesis by A5;

        end;

        hence thesis by A3, A4, YELLOW_0:def 10;

      end;

      ( rng the mapping of N) = { G(j) where j be Element of N : P[j] } by WAYBEL11: 19

      .= X from FRAENKEL:sch 5( A1);



      hence ( lim_inf N) = ( Sup the mapping of N) by YELLOW_2:def 5

      .= ( sup N) by WAYBEL_2:def 1;

    end;

    theorem :: WAYBEL32:10



     Th10: for R be /\-complete Semilattice holds for S be Subset of R holds S in the topology of ( ConvergenceSpace ( Scott-Convergence R)) iff S is inaccessible upper

    proof

      let R be /\-complete Semilattice;

      set SC = ( Scott-Convergence R), T = ( ConvergenceSpace SC);



       A1: the topology of T = { V where V be Subset of R : for p be Element of R st p in V holds for N be net of R st [N, p] in SC holds N is_eventually_in V } by YELLOW_6:def 24;

      let S be Subset of R;

      hereby

        assume S in the topology of T;

        then

         A2: ex V be Subset of R st (S = V) & (for p be Element of R st p in V holds for N be net of R st [N, p] in SC holds N is_eventually_in V) by A1;

        thus S is inaccessible

        proof

          let D be non empty directed Subset of R such that

           A3: ( sup D) in S;



           A4: ( dom ( id D)) = D by RELAT_1: 45;



           A5: ( rng ( id D)) = D by RELAT_1: 45;

          then

          reconsider f = ( id D) as Function of D, the carrier of R by A4, FUNCT_2:def 1, RELSET_1: 4;

          reconsider N = ( Net-Str (D,f)) as strict monotone reflexive net of R by A5, WAYBEL11: 20;



           A6: N in ( NetUniv R) by WAYBEL11: 21;

          ( lim_inf N) = ( sup N) by Th9

          .= ( Sup the mapping of N) by WAYBEL_2:def 1

          .= ( "\/" (( rng the mapping of N),R)) by YELLOW_2:def 5

          .= ( "\/" (( rng f),R)) by WAYBEL11:def 10

          .= ( sup D) by RELAT_1: 45;

          then ( sup D) is_S-limit_of N;

          then [N, ( sup D)] in SC by A6, WAYBEL11:def 8;

          then N is_eventually_in S by A2, A3;

          then

          consider i0 be Element of N such that

           A7: for j be Element of N st i0 <= j holds (N . j) in S;

          consider j0 be Element of N such that

           A8: j0 >= i0 and j0 >= i0 by YELLOW_6:def 3;



           A9: (N . j0) in S by A7, A8;



           A10: D = the carrier of N by WAYBEL11:def 10;

          (N . j0) = (( id D) . j0) by WAYBEL11:def 10

          .= j0 by A10;

          hence thesis by A9, A10, XBOOLE_0: 3;

        end;

        thus S is upper

        proof

          let x,y be Element of R such that

           A11: x in S and

           A12: x <= y;



           A13: ( Net-Str y) in ( NetUniv R) by WAYBEL11: 29;

          y = ( lim_inf ( Net-Str y)) by WAYBEL11: 28;

          then x is_S-limit_of ( Net-Str y) by A12;

          then [( Net-Str y), x] in SC by A13, WAYBEL11:def 8;

          then ( Net-Str y) is_eventually_in S by A2, A11;

          hence thesis by WAYBEL11: 27;

        end;

      end;

      assume that

       A14: S is inaccessible and

       A15: S is upper;

      for p be Element of R st p in S holds for N be net of R st [N, p] in SC holds N is_eventually_in S

      proof

        let p be Element of R such that

         A16: p in S;

        reconsider p9 = p as Element of R;

        let N be net of R;

        assume

         A17: [N, p] in SC;

        SC c= [:( NetUniv R), the carrier of R:] by YELLOW_6:def 18;

        then

         A18: N in ( NetUniv R) by A17, ZFMISC_1: 87;

        then ex N9 be strict net of R st N9 = N & the carrier of N9 in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

        then p is_S-limit_of N by A17, A18, WAYBEL11:def 8;

        then

         A19: p9 <= ( lim_inf N);

        deffunc F( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

        defpred P[ set] means not contradiction;

        set X = { F(j) where j be Element of N : P[j] };

        X is Subset of R from DOMAIN_1:sch 8;

        then

        reconsider D = X as Subset of R;

        reconsider D as non empty directed Subset of R by Th7;

        ( sup D) in S by A15, A16, A19;

        then D meets S by A14;

        then (D /\ S) <> {} ;

        then

        consider d be Element of R such that

         A20: d in (D /\ S) by SUBSET_1: 4;

        reconsider d as Element of R;

        d in D by A20, XBOOLE_0:def 4;

        then

        consider j be Element of N such that

         A21: d = ( "/\" ({ (N . i) where i be Element of N : i >= j },R));

        defpred P[ Element of N] means $1 >= j;

        deffunc F( Element of N) = (N . $1);

        { F(i) where i be Element of N : P[i] } is Subset of R from DOMAIN_1:sch 8;

        then

        reconsider Y = { (N . i) where i be Element of N : i >= j } as Subset of R;

        reconsider j as Element of N;

        take j;

        let i0 be Element of N;



         A22: d in S by A20, XBOOLE_0:def 4;

        assume j <= i0;

        then (N . i0) in Y;

        then d <= (N . i0) by A21, Th8;

        hence thesis by A15, A22;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL32:11



     Th11: for R be /\-complete up-complete Semilattice, T be TopAugmentation of R st the topology of T = ( sigma R) holds T is Scott

    proof

      let R be /\-complete up-complete Semilattice;

      let T be TopAugmentation of R such that

       A1: the topology of T = ( sigma R);



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

      T is Scott

      proof

        let S be Subset of T;

        reconsider A = S as Subset of R by A2;

        thus S is open implies S is inaccessible upper

        proof

          assume S is open;

          then S in the topology of T by PRE_TOPC:def 2;

          then A is inaccessible upper by A1, Th10;

          hence thesis by A2, WAYBEL_0: 25, YELLOW_9: 47;

        end;

        assume

         A3: S is inaccessible upper;

        A is inaccessible

        proof

          let D be non empty directed Subset of R such that

           A4: ( sup D) in A;

          reconsider E = D as Subset of T by A2;

          ex a be Element of R st a is_>=_than D & for b be Element of R st b is_>=_than D holds a <= b by WAYBEL_0:def 39;

          then

           A5: ex_sup_of (D,R) by YELLOW_0: 15;



           A6: E is directed by A2, WAYBEL_0: 3;

          ( sup D) = ( sup E) by A2, A5, YELLOW_0: 26;

          hence thesis by A3, A4, A6;

        end;

        then A is inaccessible upper by A2, A3, WAYBEL_0: 25;

        then A in the topology of T by A1, Th10;

        hence thesis by PRE_TOPC:def 2;

      end;

      hence thesis;

    end;

    registration

      let R be /\-complete up-complete Semilattice;

      cluster strict Scott correct for TopAugmentation of R;

      existence

      proof

        set T = TopRelStr (# the carrier of R, the InternalRel of R, ( sigma R) #);

         the RelStr of T = the RelStr of R;

        then

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

        take T;

        thus thesis by Th11, YELLOW_9: 48;

      end;

    end

    theorem :: WAYBEL32:12

    for S be up-complete /\-complete Semilattice, T be Scott TopAugmentation of S holds ( sigma S) = the topology of T

    proof

      let S be up-complete /\-complete Semilattice;

      let T be Scott TopAugmentation of S;

      thus ( sigma S) c= the topology of T

      proof

        let e be object;

        assume

         A1: e in ( sigma S);

        then

        reconsider A = e as Subset of S;



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

        then

        reconsider A9 = A as Subset of T;

        A is inaccessible upper by A1, Th10;

        then A9 is inaccessible upper by A2, WAYBEL_0: 25, YELLOW_9: 47;

        hence thesis by PRE_TOPC:def 2;

      end;

      let e be object;

      assume

       A3: e in the topology of T;

      then

      reconsider A = e as Subset of T;



       A4: A is open by A3, PRE_TOPC:def 2;



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

      then

      reconsider A9 = A as Subset of S;

      A9 is inaccessible

      proof

        let D be non empty directed Subset of S such that

         A6: ( sup D) in A9;

        reconsider E = D as Subset of T by A5;

        ex a be Element of S st a is_>=_than D & for b be Element of S st b is_>=_than D holds a <= b by WAYBEL_0:def 39;

        then

         A7: ex_sup_of (D,S) by YELLOW_0: 15;



         A8: E is directed by A5, WAYBEL_0: 3;

        ( sup D) = ( sup E) by A5, A7, YELLOW_0: 26;

        hence thesis by A4, A6, A8, WAYBEL11:def 1;

      end;

      then A9 is inaccessible upper by A4, A5, WAYBEL_0: 25;

      hence thesis by Th10;

    end;

    theorem :: WAYBEL32:13

    for T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr holds T is T_0-TopSpace

    proof

      let T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr;

      reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9: 44;

      now

        let x,y be Point of T9;

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



         A1: ( Cl {x9}) = ( downarrow x9) by Th5;



         A2: ( Cl {y9}) = ( downarrow y9) by Th5;

        assume x <> y;

        hence ( Cl {x}) <> ( Cl {y}) by A1, A2, WAYBEL_0: 19;

      end;

      hence thesis by TSP_1:def 5;

    end;

    registration

      let R be up-complete non empty reflexive transitive antisymmetric RelStr;

      cluster -> up-complete for TopAugmentation of R;

      coherence ;

    end

    theorem :: WAYBEL32:14



     Th14: for R be up-complete non empty reflexive transitive antisymmetric RelStr holds for T be Scott TopAugmentation of R, x be Element of T, A be upper Subset of T st not x in A holds (( downarrow x) ` ) is a_neighborhood of A

    proof

      let R be up-complete non empty reflexive transitive antisymmetric RelStr, T be Scott TopAugmentation of R, x be Element of T, A be upper Subset of T such that

       A1: not x in A;

      ( downarrow x) is closed by WAYBEL11: 11;

      then (( downarrow x) ` ) is open;

      then

       A2: ( Int (( downarrow x) ` )) = (( downarrow x) ` ) by TOPS_1: 23;

      A misses ( downarrow x) by A1, WAYBEL11: 5;

      then A c= (( downarrow x) ` ) by SUBSET_1: 23;

      hence thesis by A2, CONNSP_2:def 2;

    end;

    theorem :: WAYBEL32:15

    for R be up-complete non empty reflexive transitive antisymmetric TopRelStr holds for T be Scott TopAugmentation of R, S be upper Subset of T holds ex F be Subset-Family of T st S = ( meet F) & for X be Subset of T st X in F holds X is a_neighborhood of S

    proof

      let R be up-complete non empty reflexive transitive antisymmetric TopRelStr, T be Scott TopAugmentation of R, S be upper Subset of T;

      defpred P[ set] means $1 is a_neighborhood of S;

      set F = { X where X be Subset of T : P[X] };

      F is Subset-Family of T from DOMAIN_1:sch 7;

      then

      reconsider F as Subset-Family of T;

      take F;

      thus S = ( meet F)

      proof

        ( [#] T) is a_neighborhood of S by CONNSP_2: 28;

        then

         A1: ( [#] T) in F;

        now

          let Z1 be set;

          assume Z1 in F;

          then ex X be Subset of T st Z1 = X & X is a_neighborhood of S;

          hence S c= Z1 by CONNSP_2: 29;

        end;

        hence S c= ( meet F) by A1, SETFAM_1: 5;

        let x be object such that

         A2: x in ( meet F) and

         A3: not x in S;

        reconsider p = x as Element of T by A2;

        (( downarrow p) ` ) is a_neighborhood of S by A3, Th14;

        then (( downarrow p) ` ) in F;

        then

         A4: ( meet F) c= (( downarrow p) ` ) by SETFAM_1: 3;

        p <= p;

        then p in ( downarrow p) by WAYBEL_0: 17;

        hence contradiction by A2, A4, XBOOLE_0:def 5;

      end;

      let X be Subset of T;

      assume X in F;

      then ex Y be Subset of T st X = Y & Y is a_neighborhood of S;

      hence thesis;

    end;

    theorem :: WAYBEL32:16

    for T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, S be Subset of T holds S is open iff S is upper property(S)

    proof

      let T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, S be Subset of T;

      hereby

        assume

         A1: S is open;

        hence S is upper;

        thus S is property(S)

        proof

          let D be non empty directed Subset of T;

          assume ( sup D) in S;

          then S meets D by A1, WAYBEL11:def 1;

          then

          consider y be object such that

           A2: y in S and

           A3: y in D by XBOOLE_0: 3;

          reconsider y as Element of T by A2;

          take y;

          thus thesis by A1, A2, A3, WAYBEL_0:def 20;

        end;

      end;

      assume that

       A4: S is upper and

       A5: S is property(S);

      S is inaccessible

      proof

        let D be non empty directed Subset of T;

        assume ( sup D) in S;

        then

        consider y be Element of T such that

         A6: y in D and

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

        y >= y by YELLOW_0:def 1;

        then y in S by A6, A7;

        hence thesis by A6, XBOOLE_0: 3;

      end;

      hence thesis by A4;

    end;

    theorem :: WAYBEL32:17



     Th17: for R be up-complete non empty reflexive transitive antisymmetric TopRelStr, S be non empty directed Subset of R, a be Element of R holds a in S implies a <= ( "\/" (S,R))

    proof

      let R be up-complete non empty reflexive transitive antisymmetric TopRelStr;

      let S be non empty directed Subset of R, a be Element of R;

      assume

       A1: a in S;

       ex_sup_of (S,R) by WAYBEL_0: 75;

      then S is_<=_than ( "\/" (S,R)) by YELLOW_0: 30;

      hence thesis by A1;

    end;

    registration

      let T be up-complete non empty reflexive transitive antisymmetric TopRelStr;

      cluster lower -> property(S) for Subset of T;

      coherence

      proof

        let S be Subset of T;

        assume

         A1: S is lower;

        let D be non empty directed Subset of T such that

         A2: ( sup D) in S;

        consider y be Element of T such that

         A3: y in D by SUBSET_1: 4;

        take y;

        thus y in D by A3;

        let x be Element of T such that

         A4: x in D and x >= y;

        x <= ( sup D) by A4, Th17;

        hence thesis by A1, A2;

      end;

    end

    theorem :: WAYBEL32:18

    for T be finite up-complete non empty Poset, S be Subset of T holds S is inaccessible

    proof

      let T be finite up-complete non empty Poset, S be Subset of T, D be non empty directed Subset of T such that

       A1: ( sup D) in S;

      ( sup D) in D

      proof

        reconsider D9 = D as finite Subset of T;

        D9 c= D9;

        then

        reconsider E = D9 as finite Subset of D;

        consider x be Element of T such that

         A2: x in D and

         A3: x is_>=_than E by WAYBEL_0: 1;



         A4: for b be Element of T st D is_<=_than b holds b >= x by A2;

        for c be Element of T st D is_<=_than c & for b be Element of T st D is_<=_than b holds b >= c holds c = x

        proof

          let c be Element of T such that

           A5: D is_<=_than c and

           A6: for b be Element of T st D is_<=_than b holds b >= c;



           A7: x >= c by A3, A6;

          c >= x by A2, A5;

          hence thesis by A7, ORDERS_2: 2;

        end;

        then ex_sup_of (D,T) by A3, A4, YELLOW_0:def 7;

        hence thesis by A2, A3, A4, YELLOW_0:def 9;

      end;

      hence thesis by A1, XBOOLE_0: 3;

    end;

    theorem :: WAYBEL32:19



     Th19: for R be complete connected LATTICE, T be Scott TopAugmentation of R, x be Element of T holds (( downarrow x) ` ) is open

    proof

      let R be complete connected LATTICE, T be Scott TopAugmentation of R, x be Element of T;

      reconsider S = ( downarrow x) as directly_closed lower Subset of T by WAYBEL11: 8;

      (S ` ) is open;

      hence thesis;

    end;

    theorem :: WAYBEL32:20

    for R be complete connected LATTICE, T be Scott TopAugmentation of R, S be Subset of T holds S is open iff S = the carrier of T or S in the set of all (( downarrow x) ` ) where x be Element of T

    proof

      let R be complete connected LATTICE, T be Scott TopAugmentation of R, S be Subset of T;

      set DD = the set of all (( downarrow x) ` ) where x be Element of T;

      thus S is open implies S = the carrier of T or S in DD

      proof

        assume

         A1: S is open;

        assume that

         A2: S <> the carrier of T and

         A3: not S in DD;



         A4: (( [#] T) \ S) <> {} by A2, PRE_TOPC: 4;



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

        then

        reconsider K = (S ` ) as Subset of R;

        reconsider D = K as non empty directed Subset of T by A4, A5, WAYBEL_0: 3;



         A6: D misses S by SUBSET_1: 23;

        reconsider x = ( sup D) as Element of T;

        (S ` ) = ( downarrow x)

        proof

          thus (S ` ) c= ( downarrow x)

          proof

            let a be object;

            assume

             A7: a in (S ` );

            then

            reconsider A = a as Element of T;

            x is_>=_than (S ` ) by YELLOW_0: 32;

            then A <= x by A7;

            hence thesis by WAYBEL_0: 17;

          end;

          let a be object;

          assume

           A8: a in ( downarrow x);

          then

          reconsider A = a as Element of T;



           A9: A <= x by A8, WAYBEL_0: 17;

           not x in S by A1, A6, WAYBEL11:def 1;

          then not A in S by A1, A9, WAYBEL_0:def 20;

          hence thesis by XBOOLE_0:def 5;

        end;

        then (( downarrow x) ` ) = S;

        hence contradiction by A3;

      end;

      assume

       A10: S = the carrier of T or S in DD;

      per cases by A10;

        suppose

         A11: S = the carrier of T;



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

        then S = ( [#] R) by A11;

        then

         A13: S is inaccessible by A12, YELLOW_9: 47;

        S is upper by A11;

        hence thesis by A13;

      end;

        suppose S in DD;

        then ex x be Element of T st (S = (( downarrow x) ` ));

        hence thesis by Th19;

      end;

    end;

    registration

      let R be up-complete non empty Poset;

      cluster order_consistent for correct TopAugmentation of R;

      correctness

      proof

        set T = the Scott correct TopAugmentation of R;

        take T;

        thus thesis by Th6;

      end;

    end

    registration

      cluster order_consistent complete for TopLattice;

      correctness

      proof

        set T = the Scott complete TopLattice;

        take T;

        thus thesis by Th6;

      end;

    end

    theorem :: WAYBEL32:21



     Th21: for R be non empty TopRelStr holds for A be Subset of R holds (for x be Element of R holds ( downarrow x) = ( Cl {x})) implies (A is open implies A is upper)

    proof

      let R be non empty TopRelStr, A be Subset of R;

      assume

       A1: for x be Element of R holds ( downarrow x) = ( Cl {x});

      assume

       A2: A is open;

      let x,y be Element of R such that

       A3: x in A and

       A4: x <= y;

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

      then x in ( Cl {y}) by A1;

      then A meets {y} by A2, A3, PRE_TOPC: 24;

      then

      consider z be object such that

       A5: z in (A /\ {y}) by XBOOLE_0: 4;



       A6: z in A by A5, XBOOLE_0:def 4;

      z in {y} by A5, XBOOLE_0:def 4;

      hence thesis by A6, TARSKI:def 1;

    end;

    theorem :: WAYBEL32:22

    for R be non empty TopRelStr holds for A be Subset of R holds (for x be Element of R holds ( downarrow x) = ( Cl {x})) implies for A be Subset of R st A is closed holds A is lower

    proof

      let R be non empty TopRelStr, A be Subset of R;

      assume

       A1: for x be Element of R holds ( downarrow x) = ( Cl {x});

      let A be Subset of R such that

       A2: A is closed;

      let x,y be Element of R such that

       A3: x in A and

       A4: y <= x;

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

      then

       A5: y in ( Cl {x}) by A1;

       {x} c= A by A3, TARSKI:def 1;

      hence thesis by A2, A5, PRE_TOPC: 15;

    end;

    definition

      let S be non empty 1-sorted, R be non empty RelStr, f be Function of the carrier of R, the carrier of S;

      :: WAYBEL32:def3

      func R *' f -> strict non empty NetStr over S means

      : Def3: the RelStr of it = the RelStr of R & the mapping of it = f;

      existence

      proof

        reconsider M = NetStr (# the carrier of R, the InternalRel of R, f #) as strict non empty NetStr over S;

        take M;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let S be non empty 1-sorted, R be non empty transitive RelStr, f be Function of the carrier of R, the carrier of S;

      cluster (R *' f) -> transitive;

      coherence

      proof

         the RelStr of (R *' f) = the RelStr of R by Def3;

        hence thesis by WAYBEL_8: 13;

      end;

    end

    registration

      let S be non empty 1-sorted, R be non empty directed RelStr, f be Function of the carrier of R, the carrier of S;

      cluster (R *' f) -> directed;

      coherence

      proof



         A1: the RelStr of (R *' f) = the RelStr of R by Def3;

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

        hence ( [#] (R *' f)) is directed by A1, WAYBEL_0: 3;

      end;

    end

    definition

      let R be non empty RelStr, N be prenet of R;

      :: WAYBEL32:def4

      func inf_net N -> strict prenet of R means

      : Def4: ex f be Function of N, R st it = (N *' f) & for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R));

      existence

      proof

        deffunc F( Element of N) = ( "/\" ({ (N . k) where k be Element of N : k >= $1 },R));

        consider g be Function of the carrier of N, the carrier of R such that

         A1: for i be Element of N holds (g . i) = F(i) from FUNCT_2:sch 4;

        reconsider f = g as Function of N, R;

        reconsider M = (N *' f) as strict prenet of R;

        take M;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let M,P be strict prenet of R such that

         A2: ex f be Function of N, R st M = (N *' f) & for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) and

         A3: ex f be Function of N, R st P = (N *' f) & for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R));

        consider f1 be Function of N, R such that

         A4: M = (N *' f1) and

         A5: for i be Element of N holds (f1 . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by A2;

        consider f2 be Function of N, R such that

         A6: P = (N *' f2) and

         A7: for i be Element of N holds (f2 . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by A3;

        for i be object st i in the carrier of N holds (f1 . i) = (f2 . i)

        proof

          let i be object;

          assume i in the carrier of N;

          then

          reconsider i as Element of N;

          (f1 . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by A5

          .= (f2 . i) by A7;

          hence thesis;

        end;

        hence thesis by A4, A6, FUNCT_2: 12;

      end;

    end

    registration

      let R be non empty RelStr, N be net of R;

      cluster ( inf_net N) -> transitive;

      coherence

      proof

        ex f be Function of N, R st ( inf_net N) = (N *' f) & for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by Def4;

        hence thesis;

      end;

    end

    registration

      let R be non empty RelStr, N be net of R;

      cluster ( inf_net N) -> directed;

      coherence ;

    end

    registration

      let R be /\-complete non empty reflexive antisymmetric RelStr, N be net of R;

      cluster ( inf_net N) -> monotone;

      coherence

      proof

        let i,j be Element of ( inf_net N) such that

         A1: i <= j;

        consider f be Function of N, R such that

         A2: ( inf_net N) = (N *' f) and

         A3: for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by Def4;



         A4: the RelStr of ( inf_net N) = the RelStr of N by A2, Def3;

        then

        reconsider i9 = i, j9 = j as Element of N;

        deffunc F( Element of N) = (N . $1);

        defpred P[ Element of N] means $1 >= j9;

        defpred Q[ Element of N] means $1 >= i9;

        set J = { F(k) where k be Element of N : P[k] };

        set I = { F(k) where k be Element of N : Q[k] };



         A5: J is Subset of R from DOMAIN_1:sch 8;

        consider j0 be Element of N such that

         A6: j0 >= j9 and j0 >= j9 by YELLOW_6:def 3;

        (N . j0) in J by A6;

        then

        reconsider J9 = J as non empty Subset of R by A5;



         A7: I is Subset of R from DOMAIN_1:sch 8;

        consider j1 be Element of N such that

         A8: j1 >= i9 and j1 >= i9 by YELLOW_6:def 3;

        (N . j1) in I by A8;

        then

        reconsider I9 = I as non empty Subset of R by A7;



         A9: ex_inf_of (J9,R) by WAYBEL_0: 76;



         A10: ex_inf_of (I9,R) by WAYBEL_0: 76;



         A11: J9 c= I9

        proof

          let a be object;

          assume

           A12: a in J9;

          then

          reconsider x = a as Element of R;

          consider k be Element of N such that

           A13: x = (N . k) and

           A14: k >= j9 by A12;

          reconsider k9 = k as Element of N;

          i9 <= j9 by A1, A4, YELLOW_0: 1;

          then i9 <= k9 by A14, YELLOW_0:def 2;

          hence thesis by A13;

        end;



         A15: (f . i9) = ( "/\" (I,R)) by A3;



         A16: (f . j9) = ( "/\" (J,R)) by A3;

        the mapping of ( inf_net N) = f by A2, Def3;

        hence thesis by A9, A10, A11, A15, A16, YELLOW_0: 35;

      end;

    end

    registration

      let R be /\-complete non empty reflexive antisymmetric RelStr, N be net of R;

      cluster ( inf_net N) -> eventually-directed;

      coherence ;

    end

    theorem :: WAYBEL32:23



     Th23: for R be non empty RelStr, N be net of R holds ( rng the mapping of ( inf_net N)) = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },R)) where j be Element of N

    proof

      let R be non empty RelStr, N be net of R;

      consider f be Function of N, R such that

       A1: ( inf_net N) = (N *' f) and

       A2: for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by Def4;



       A3: the RelStr of ( inf_net N) = the RelStr of N by A1, Def3;



       A4: the mapping of ( inf_net N) = f by A1, Def3;

      then

       A5: the carrier of ( inf_net N) = ( dom f) by FUNCT_2:def 1;

      thus ( rng the mapping of ( inf_net N)) c= the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },R)) where j be Element of N

      proof

        let e be object;

        assume e in ( rng the mapping of ( inf_net N));

        then

        consider u be object such that

         A6: u in ( dom f) and

         A7: e = (f . u) by A4, FUNCT_1:def 3;

        reconsider u as Element of N by A6;

        (f . u) = ( "/\" ({ (N . k) where k be Element of N : k >= u },R)) by A2;

        hence thesis by A7;

      end;

      let e be object;

      assume e in the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },R)) where j be Element of N;

      then

      consider j be Element of N such that

       A8: e = ( "/\" ({ (N . i) where i be Element of N : i >= j },R));

      e = (the mapping of ( inf_net N) . j) by A2, A4, A8;

      hence thesis by A3, A4, A5, FUNCT_1:def 3;

    end;

    theorem :: WAYBEL32:24



     Th24: for R be up-complete /\-complete LATTICE, N be net of R holds ( sup ( inf_net N)) = ( lim_inf N)

    proof

      let R be up-complete /\-complete LATTICE, N be net of R;

      defpred P[ set] means not contradiction;

      deffunc F( Element of N) = ( "/\" ({ (N . l) where l be Element of N : l >= $1 },R));

      ( sup ( inf_net N)) = ( Sup the mapping of ( inf_net N)) by WAYBEL_2:def 1

      .= ( sup ( rng the mapping of ( inf_net N))) by YELLOW_2:def 5

      .= ( lim_inf N) by Th23;

      hence thesis;

    end;

    theorem :: WAYBEL32:25

    for R be up-complete /\-complete LATTICE, N be net of R, i be Element of N holds ( sup ( inf_net N)) = ( lim_inf (N | i))

    proof

      let R be up-complete /\-complete LATTICE, N be net of R, i be Element of N;

      ( sup ( inf_net N)) = ( lim_inf N) by Th24;

      hence thesis by WAYBEL21: 41;

    end;

    theorem :: WAYBEL32:26



     Th26: for R be /\-complete Semilattice, N be net of R, V be upper Subset of R holds ( inf_net N) is_eventually_in V implies N is_eventually_in V

    proof

      let R be /\-complete Semilattice, N be net of R, V be upper Subset of R;

      consider f be Function of N, R such that

       A1: ( inf_net N) = (N *' f) and

       A2: for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by Def4;



       A3: the RelStr of ( inf_net N) = the RelStr of N by A1, Def3;

      assume ( inf_net N) is_eventually_in V;

      then

      consider i be Element of ( inf_net N) such that

       A4: for j be Element of ( inf_net N) st i <= j holds (( inf_net N) . j) in V;

      consider j0 be Element of ( inf_net N) such that

       A5: i <= j0 and i <= j0 by YELLOW_6:def 3;



       A6: (( inf_net N) . j0) in V by A4, A5;

      reconsider j9 = j0 as Element of N by A3;

      take j9;

      let j be Element of N such that

       A7: j9 <= j;

      defpred P[ Element of N] means $1 >= j9;

      deffunc F( Element of N) = (N . $1);

      set E = { F(k) where k be Element of N : P[k] };

      E is Subset of R from DOMAIN_1:sch 8;

      then

      reconsider E as Subset of R;

      the mapping of ( inf_net N) = f by A1, Def3;

      then

       A8: (( inf_net N) . j0) = ( "/\" (E,R)) by A2;

      (N . j) in E by A7;

      then ( "/\" (E,R)) <= (N . j) by Th8;

      hence thesis by A6, A8, WAYBEL_0:def 20;

    end;

    theorem :: WAYBEL32:27

    for R be /\-complete Semilattice, N be net of R, V be lower Subset of R holds N is_eventually_in V implies ( inf_net N) is_eventually_in V

    proof

      let R be /\-complete Semilattice, N be net of R, V be lower Subset of R;

      consider f be Function of N, R such that

       A1: ( inf_net N) = (N *' f) and

       A2: for i be Element of N holds (f . i) = ( "/\" ({ (N . k) where k be Element of N : k >= i },R)) by Def4;



       A3: the RelStr of ( inf_net N) = the RelStr of N by A1, Def3;

      assume N is_eventually_in V;

      then

      consider i be Element of N such that

       A4: for j be Element of N st i <= j holds (N . j) in V;

      reconsider i9 = i as Element of ( inf_net N) by A3;

      take i9;

      let j be Element of ( inf_net N) such that

       A5: i9 <= j;

      reconsider j0 = j as Element of N by A3;

      defpred P[ Element of N] means $1 >= j0;

      deffunc F( Element of N) = (N . $1);

      set E = { F(k) where k be Element of N : P[k] };

      consider j1 be Element of N such that

       A6: j1 >= j0 and j1 >= j0 by YELLOW_6:def 3;

      E is Subset of R from DOMAIN_1:sch 8;

      then

      reconsider E as Subset of R;

      i <= j0 by A3, A5, YELLOW_0: 1;

      then i <= j1 by A6, YELLOW_0:def 2;

      then

       A7: (N . j1) in V by A4;

      (N . j1) in E by A6;

      then

       A8: ( "/\" (E,R)) <= (N . j1) by Th8;

      the mapping of ( inf_net N) = f by A1, Def3;

      then (( inf_net N) . j) = ( "/\" (E,R)) by A2;

      hence thesis by A7, A8, WAYBEL_0:def 19;

    end;

    theorem :: WAYBEL32:28



     Th28: for R be order_consistent up-complete /\-complete non empty TopLattice holds for N be net of R, x be Element of R holds x <= ( lim_inf N) implies x is_a_cluster_point_of N

    proof

      let R be order_consistent up-complete /\-complete non empty TopLattice, N be net of R, x be Element of R;

      assume

       A1: x <= ( lim_inf N);

      defpred P[ Element of N] means not contradiction;

      deffunc F( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

      set X = { F(j) where j be Element of N : P[j] };

      X is Subset of R from DOMAIN_1:sch 8;

      then

      reconsider D = X as Subset of R;

      reconsider D as non empty directed Subset of R by Th7;

      ( sup D) = ( lim_inf N);

      then

       A2: ( sup D) = ( sup ( inf_net N)) by Th24;

      let V be a_neighborhood of x;

      for a be Element of R holds ( downarrow a) = ( Cl {a}) by Def2;

      then

       A3: ( Int V) is upper by Th21;

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

      then ( sup D) in ( Int V) by A1, A3;

      then

      reconsider W = ( Int V) as a_neighborhood of ( sup D) by CONNSP_2: 3;



       A4: ( Int V) c= V by TOPS_1: 16;

      ( inf_net N) is_eventually_in W by A2, Def2;

      then N is_eventually_in W by A3, Th26;

      then N is_eventually_in V by A4, WAYBEL_0: 8;

      hence thesis by YELLOW_6: 19;

    end;

    theorem :: WAYBEL32:29

    for R be order_consistent up-complete /\-complete non empty TopLattice holds for N be eventually-directed net of R, x be Element of R holds x <= ( lim_inf N) iff x is_a_cluster_point_of N

    proof

      let R be order_consistent up-complete /\-complete non empty TopLattice, N be eventually-directed net of R, x be Element of R;

      thus x <= ( lim_inf N) implies x is_a_cluster_point_of N by Th28;

      thus x is_a_cluster_point_of N implies x <= ( lim_inf N)

      proof

        assume

         A1: x is_a_cluster_point_of N;

        defpred P[ Element of N] means not contradiction;

        deffunc F( Element of N) = ( "/\" ({ (N . i) where i be Element of N : i >= $1 },R));

        set X = { F(j) where j be Element of N : P[j] };

        X is Subset of R from DOMAIN_1:sch 8;

        then

        reconsider D = X as Subset of R;

        reconsider D as non empty directed Subset of R by Th7;

        for G be Subset of R st G is open holds x in G implies {( sup D)} meets G

        proof

          let G be Subset of R such that

           A2: G is open;

          assume x in G;

          then

          reconsider G as a_neighborhood of x by A2, CONNSP_2: 3;



           A3: N is_often_in G by A1;

          now

            let i be Element of N;

            consider j1 be Element of N such that i <= j1 and

             A4: (N . j1) in G by A3;

            consider j2 be Element of N such that

             A5: for k be Element of N st j2 <= k holds (N . j1) <= (N . k) by WAYBEL_0: 11;

            defpred P[ Element of N] means $1 >= j2;

            deffunc F( Element of N) = (N . $1);

            set E = { F(k) where k be Element of N : P[k] };



             A6: E is Subset of R from DOMAIN_1:sch 8;

            consider j9 be Element of N such that

             A7: j9 >= j2 and j9 >= j2 by YELLOW_6:def 3;

            (N . j9) in E by A7;

            then

            reconsider E9 = E as non empty Subset of R by A6;



             A8: ex_inf_of (E9,R) by WAYBEL_0: 76;

            (N . j1) is_<=_than E9

            proof

              let b be Element of R;

              assume b in E9;

              then ex k be Element of N st (b = (N . k)) & (k >= j2);

              hence (N . j1) <= b by A5;

            end;

            then

             A9: (N . j1) <= ( "/\" (E9,R)) by A8, YELLOW_0: 31;

            for a be Element of R holds ( downarrow a) = ( Cl {a}) by Def2;

            then

             A10: G is upper by A2, Th21;

            then

             A11: ( "/\" (E9,R)) in G by A4, A9;

            ( "/\" (E9,R)) in D;

            then ( "/\" (E9,R)) <= ( sup D) by Th17;

            hence ( sup D) in G by A10, A11;

          end;

          then

           A12: ( sup D) in G;

          ( sup D) in {( sup D)} by TARSKI:def 1;

          hence thesis by A12, XBOOLE_0: 3;

        end;

        then x in ( Cl {( sup D)}) by PRE_TOPC: 24;

        then x in ( downarrow ( sup D)) by Def2;

        hence thesis by WAYBEL_0: 17;

      end;

    end;