waybel11.miz



    begin

    

     Lm1: for R,S be RelStr, p,q be Element of R, p9,q9 be Element of S st p = p9 & q = q9 & the RelStr of R = the RelStr of S holds p <= q implies p9 <= q9

    proof

      let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that

       A1: p = p9 and

       A2: q = q9 and

       A3: the RelStr of R = the RelStr of S;

      assume p <= q;

      then [p9, q9] in the InternalRel of S by A1, A2, A3, ORDERS_2:def 5;

      hence thesis by ORDERS_2:def 5;

    end;

    scheme :: WAYBEL11:sch1

    Irrel { D,I() -> non empty set , P[ set], F( set) -> set , F( set, set) -> set } :

{ F(u) where u be Element of D() : P[u] } = { F(i,v) where i be Element of I(), v be Element of D() : P[v] }

      provided

       A1: for i be Element of I(), u be Element of D() holds F(u) = F(i,u);

      set A = { F(u) where u be Element of D() : P[u] }, B = { F(i,v) where i be Element of I(), v be Element of D() : P[v] };

      thus A c= B

      proof

        let e be object;

        set i = the Element of I();

        assume e in A;

        then

        consider u be Element of D() such that

         A2: e = F(u) and

         A3: P[u];

        e = F(i,u) by A1, A2;

        hence thesis by A3;

      end;

      let e be object;

      assume e in B;

      then

      consider i be Element of I(), u be Element of D() such that

       A4: e = F(i,u) and

       A5: P[u];

      e = F(u) by A1, A4;

      hence thesis by A5;

    end;

    theorem :: WAYBEL11:1

    

     Th1: for L be complete LATTICE, X,Y be Subset of L st Y is_coarser_than X holds ( "/\" (X,L)) <= ( "/\" (Y,L))

    proof

      let L be complete LATTICE, X,Y be Subset of L such that

       A1: Y is_coarser_than X;

      ( "/\" (X,L)) is_<=_than Y

      proof

        let y be Element of L;

        assume y in Y;

        then

        consider x be Element of L such that

         A2: x in X and

         A3: x <= y by A1;

        ( "/\" (X,L)) <= x by A2, YELLOW_2: 22;

        hence ( "/\" (X,L)) <= y by A3, YELLOW_0:def 2;

      end;

      hence thesis by YELLOW_0: 33;

    end;

    theorem :: WAYBEL11:2

    

     Th2: for L be complete LATTICE, X,Y be Subset of L st X is_finer_than Y holds ( "\/" (X,L)) <= ( "\/" (Y,L))

    proof

      let L be complete LATTICE, X,Y be Subset of L such that

       A1: X is_finer_than Y;

      ( "\/" (Y,L)) is_>=_than X

      proof

        let x be Element of L;

        assume x in X;

        then

        consider y be Element of L such that

         A2: y in Y and

         A3: x <= y by A1;

        ( "\/" (Y,L)) >= y by A2, YELLOW_2: 22;

        hence thesis by A3, YELLOW_0:def 2;

      end;

      hence thesis by YELLOW_0: 32;

    end;

    theorem :: WAYBEL11:3

    for T be RelStr, A be upper Subset of T, B be directed Subset of T holds (A /\ B) is directed

    proof

      let T be RelStr, A be upper Subset of T, B be directed Subset of T;

      let x,y be Element of T such that

       A1: x in (A /\ B) and

       A2: y in (A /\ B);

      

       A3: x in B by A1, XBOOLE_0:def 4;

      y in B by A2, XBOOLE_0:def 4;

      then

      consider z be Element of T such that

       A4: z in B and

       A5: x <= z and

       A6: y <= z by A3, WAYBEL_0:def 1;

      take z;

      x in A by A1, XBOOLE_0:def 4;

      then z in A by A5, WAYBEL_0:def 20;

      hence z in (A /\ B) by A4, XBOOLE_0:def 4;

      thus thesis by A5, A6;

    end;

    registration

      let T be reflexive non empty RelStr;

      cluster non empty directed finite for Subset of T;

      existence

      proof

        set x = the Element of T;

        take {x};

        thus thesis by WAYBEL_0: 5;

      end;

    end

    theorem :: WAYBEL11:4

    

     Th4: for T be with_suprema Poset, D be non empty directed finite Subset of T holds ( sup D) in D

    proof

      let T be reflexive transitive antisymmetric with_suprema RelStr, D be non empty directed finite Subset of T;

      D c= D;

      then

      reconsider E = D as finite Subset of D;

      consider x be Element of T such that

       A1: x in D and

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

      

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

      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

         A4: D is_<=_than c and

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

        

         A6: x >= c by A2, A5;

        c >= x by A1, A4;

        hence thesis by A6, ORDERS_2: 2;

      end;

      then ex_sup_of (D,T) by A2, A3;

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

    end;

    registration

      cluster reflexive transitive1 -element antisymmetric with_suprema with_infima finite strict for RelStr;

      existence

      proof

         0 in { 0 } by TARSKI:def 1;

        then

        reconsider r = { [ 0 , 0 ]} as Relation of { 0 } by RELSET_1: 3;

        reconsider T = RelStr (# { 0 }, r #) as non empty RelStr;

        take T;

        thus T is reflexive

        proof

          let x be Element of T;

          x = 0 by TARSKI:def 1;

          then [x, x] in { [ 0 , 0 ]} by TARSKI:def 1;

          hence thesis by ORDERS_2:def 5;

        end;

        then

        reconsider T9 = T as 1 -element reflexive RelStr;

        T9 is transitive;

        hence T is transitive;

        thus T is 1 -element;

        T9 is antisymmetric;

        hence T is antisymmetric;

        T9 is with_suprema;

        hence T is with_suprema;

        T9 is with_infima;

        hence T is with_infima;

        thus T is finite;

        thus thesis;

      end;

    end

    registration

      let T be finite 1-sorted;

      cluster -> finite for Subset of T;

      coherence ;

    end

    registration

      let R be RelStr;

      cluster empty -> lower upper for Subset of R;

      coherence ;

    end

    registration

      let R be 1 -element RelStr;

      cluster -> upper for Subset of R;

      coherence

      proof

        let S be Subset of R;

        ex x be Element of R st (the carrier of R = {x}) by TEX_1:def 1;

        then S = ( {} R) or S = ( [#] R) by ZFMISC_1: 33;

        hence thesis;

      end;

    end

    theorem :: WAYBEL11:5

    

     Th5: for T be non empty RelStr, x be Element of T, A be upper Subset of T st not x in A holds A misses ( downarrow x)

    proof

      let T be non empty RelStr, x be Element of T, A be upper Subset of T such that

       A1: not x in A;

      assume A meets ( downarrow x);

      then

      consider y be object such that

       A2: y in A and

       A3: y in ( downarrow x) by XBOOLE_0: 3;

      reconsider y as Element of T by A2;

      y <= x by A3, WAYBEL_0: 17;

      hence contradiction by A1, A2, WAYBEL_0:def 20;

    end;

    theorem :: WAYBEL11:6

    

     Th6: for T be non empty RelStr, x be Element of T, A be lower Subset of T st x in A holds ( downarrow x) c= A

    proof

      let T be non empty RelStr, x be Element of T, A be lower Subset of T;

      assume x in A;

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

      then (A ` ) misses ( downarrow x) by Th5;

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

      hence thesis by SUBSET_1: 12;

    end;

    begin

    definition

      let T be non empty reflexive RelStr, S be Subset of T;

      :: WAYBEL11:def1

      attr S is inaccessible_by_directed_joins means

      : Def1: for D be non empty directed Subset of T st ( sup D) in S holds D meets S;

      :: WAYBEL11:def2

      attr S is closed_under_directed_sups means

      : Def2: for D be non empty directed Subset of T st D c= S holds ( sup D) in S;

      :: WAYBEL11:def3

      attr S is property(S) means

      : Def3: for D be non empty directed Subset of T st ( sup D) in S 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 S;

    end

    notation

      let T be non empty reflexive RelStr, S be Subset of T;

      synonym S is inaccessible for S is inaccessible_by_directed_joins;

      synonym S is directly_closed for S is closed_under_directed_sups;

    end

    registration

      let T be non empty reflexive RelStr;

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

      coherence ;

    end

    registration

      let T be non empty reflexive RelStr;

      cluster property(S) directly_closed for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    registration

      let T be non empty reflexive RelStr, S be property(S) Subset of T;

      cluster (S ` ) -> directly_closed;

      coherence

      proof

        let D be non empty directed Subset of T such that

         A1: D c= (S ` );

        assume not ( sup D) in (S ` );

        then ( sup D) in S by XBOOLE_0:def 5;

        then

        consider y be Element of T such that

         A2: y in D and

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

        y <= y;

        then y in S by A2, A3;

        then (D /\ S) <> {} by A2, XBOOLE_0:def 4;

        then D meets S;

        hence contradiction by A1, SUBSET_1: 23;

      end;

    end

    definition

      let T be reflexive non empty TopRelStr;

      :: WAYBEL11:def4

      attr T is Scott means

      : Def4: for S be Subset of T holds S is open iff S is inaccessible upper;

    end

    registration

      let T be reflexive transitive antisymmetric non empty with_suprema finite RelStr;

      cluster -> inaccessible for Subset of T;

      coherence

      proof

        let S be Subset of T, D be non empty directed Subset of T such that

         A1: ( sup D) in S;

        ( sup D) in D by Th4;

        hence thesis by A1, XBOOLE_0: 3;

      end;

    end

    definition

      let T be reflexive transitive antisymmetric non empty with_suprema finite TopRelStr;

      :: original: Scott

      redefine

      :: WAYBEL11:def5

      attr T is Scott means for S be Subset of T holds S is open iff S is upper;

      compatibility ;

    end

    registration

      cluster complete strict1 -element Scott for TopLattice;

      existence

      proof

        set T = the reflexive1 -element discrete strict finite TopRelStr;

        take T;

        thus T is complete strict1 -element;

        let S be Subset of T;

        thus thesis by TDLAT_3: 15;

      end;

    end

    registration

      let T be non empty reflexive RelStr;

      cluster ( [#] T) -> directly_closed inaccessible;

      coherence

      proof

        thus ( [#] T) is directly_closed;

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

        ex p be Element of T st (p in D) by SUBSET_1: 4;

        hence D meets ( [#] T) by XBOOLE_0: 3;

      end;

    end

    registration

      let T be non empty reflexive RelStr;

      cluster directly_closed lower inaccessible upper for Subset of T;

      existence

      proof

        take ( [#] T);

        thus thesis;

      end;

    end

    registration

      let T be non empty reflexive RelStr, S be inaccessible Subset of T;

      cluster (S ` ) -> directly_closed;

      coherence

      proof

        let D be non empty directed Subset of T;

        assume D c= (S ` );

        then D misses S by SUBSET_1: 23;

        then not ( sup D) in S by Def1;

        hence thesis by XBOOLE_0:def 5;

      end;

    end

    registration

      let T be non empty reflexive RelStr, S be directly_closed Subset of T;

      cluster (S ` ) -> inaccessible;

      coherence

      proof

        let D be non empty directed Subset of T;

        assume ( sup D) in (S ` );

        then not ( sup D) in S by XBOOLE_0:def 5;

        then not D c= ((S ` ) ` ) by Def2;

        hence thesis by SUBSET_1: 23;

      end;

    end

    theorem :: WAYBEL11:7

    

     Th7: for T be up-complete Scott non empty reflexive transitive TopRelStr, S be Subset of T holds S is closed iff S is directly_closed lower

    proof

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

      hereby

        assume S is closed;

        then (S ` ) is open;

        then

        reconsider A = (S ` ) as inaccessible upper Subset of T by Def4;

        (A ` ) is directly_closed lower;

        hence S is directly_closed lower;

      end;

      assume S is directly_closed lower;

      then

      reconsider S as directly_closed lower Subset of T;

      (S ` ) is open by Def4;

      hence thesis;

    end;

    theorem :: WAYBEL11:8

    

     Th8: for T be up-complete non empty reflexive transitive antisymmetric TopRelStr, x be Element of T holds ( downarrow x) is directly_closed

    proof

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

      ( downarrow x) is directly_closed

      proof

        let D be non empty directed Subset of T;

        assume

         A1: D c= ( downarrow x);

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

        then

         A2: ex_sup_of (D,T) by YELLOW_0: 15;

        x is_>=_than D by A1, WAYBEL_0: 17;

        then ( sup D) <= x by A2, YELLOW_0: 30;

        hence thesis by WAYBEL_0: 17;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL11:9

    

     Th9: for T be complete Scott TopLattice, x be Element of T holds ( Cl {x}) = ( downarrow x)

    proof

      let T be complete Scott TopLattice, x be Element of T;

      ( downarrow x) is directly_closed by Th8;

      then

       A1: ( downarrow x) is closed by Th7;

      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 T such that

         A3: {x} c= C;

        reconsider D = C as Subset of T;

        assume C is closed;

        then

         A4: D is lower by Th7;

        x in C by A3, ZFMISC_1: 31;

        hence ( downarrow x) c= C by A4, Th6;

      end;

      hence thesis by A1, A2, YELLOW_8: 8;

    end;

    theorem :: WAYBEL11:10

    for T be complete Scott TopLattice holds T is T_0-TopSpace

    proof

      let T be complete Scott TopLattice;

      now

        let x,y be Point of T;

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

        

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

        

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

        assume x <> y;

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

      end;

      hence thesis by TSP_1:def 5;

    end;

    theorem :: WAYBEL11:11

    

     Th11: for T be Scott up-complete non empty reflexive transitive antisymmetric TopRelStr, x be Element of T holds ( downarrow x) is closed by Th8, Th7;

    theorem :: WAYBEL11:12

    

     Th12: for T be up-complete Scott TopLattice, x be Element of T holds (( downarrow x) ` ) is open

    proof

      let T be up-complete Scott TopLattice, x be Element of T;

      ( downarrow x) is closed by Th11;

      hence thesis;

    end;

    theorem :: WAYBEL11:13

    

     Th13: for T be up-complete Scott TopLattice, 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 T be up-complete Scott TopLattice, x be Element of T, A be upper Subset of T such that

       A1: not x in A;

      (( downarrow x) ` ) is open by Th12;

      then

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

      A misses ( downarrow x) by A1, Th5;

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

      hence thesis by A2, CONNSP_2:def 2;

    end;

    theorem :: WAYBEL11:14

    for T be complete Scott TopLattice, 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 T be complete Scott TopLattice, 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, Th13;

        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 :: WAYBEL11:15

    for T be Scott TopLattice, S be Subset of T holds S is open iff S is upper property(S)

    proof

      let T be Scott TopLattice, S be Subset of T;

      hereby

        assume

         A1: S is open;

        hence

         A2: S is upper by Def4;

        thus S is property(S)

        proof

          let D be non empty directed Subset of T such that

           A3: ( sup D) in S;

          S is inaccessible by A1, Def4;

          then S meets D by A3;

          then

          consider y be object such that

           A4: y in S and

           A5: y in D by XBOOLE_0: 3;

          reconsider y as Element of T by A4;

          take y;

          thus thesis by A2, A4, A5;

        end;

      end;

      assume that

       A6: S is upper and

       A7: 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

         A8: y in D and

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

        y >= y by YELLOW_0:def 1;

        then y in S by A8, A9;

        hence thesis by A8, XBOOLE_0: 3;

      end;

      hence thesis by A6, Def4;

    end;

    registration

      let T be complete TopLattice;

      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, YELLOW_2: 22;

        hence thesis by A1, A2;

      end;

    end

    

     Lm2: for T be non empty reflexive TopRelStr holds ( [#] T) is property(S)

    proof

      let T be non empty reflexive TopRelStr;

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

      consider y be Element of T such that

       A1: y in D by SUBSET_1: 4;

      take y;

      thus y in D by A1;

      let x be Element of T such that x in D and x >= y;

      thus thesis;

    end;

    theorem :: WAYBEL11:16

    for T be non empty transitive reflexive TopRelStr st the topology of T = { S where S be Subset of T : S is property(S) } holds T is TopSpace-like

    proof

      let T be non empty transitive reflexive TopRelStr such that

       A1: the topology of T = { S where S be Subset of T : S is property(S) };

      ( [#] T) is property(S) by Lm2;

      hence the carrier of T in the topology of T by A1;

      hereby

        let a be Subset-Family of T such that

         A2: a c= the topology of T;

        ( union a) is property(S)

        proof

          let D be non empty directed Subset of T;

          assume ( sup D) in ( union a);

          then

          consider x be set such that

           A3: ( sup D) in x and

           A4: x in a by TARSKI:def 4;

          x in the topology of T by A2, A4;

          then

          consider X be Subset of T such that

           A5: x = X and

           A6: X is property(S) by A1;

          consider y be Element of T such that

           A7: y in D and

           A8: for x be Element of T st x in D & x >= y holds x in X by A3, A5, A6;

          take y;

          thus y in D by A7;

          let u be Element of T;

          assume that

           A9: u in D and

           A10: u >= y;

          u in X by A8, A9, A10;

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

        end;

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

      end;

      let a,b be Subset of T;

      assume a in the topology of T;

      then

      consider A be Subset of T such that

       A11: a = A and

       A12: A is property(S) by A1;

      assume b in the topology of T;

      then

      consider B be Subset of T such that

       A13: b = B and

       A14: B is property(S) by A1;

      (A /\ B) is property(S)

      proof

        let D be non empty directed Subset of T;

        assume

         A15: ( sup D) in (A /\ B);

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

        then

        consider x be Element of T such that

         A16: x in D and

         A17: for z be Element of T st z in D & z >= x holds z in A by A12;

        ( sup D) in B by A15, XBOOLE_0:def 4;

        then

        consider y be Element of T such that

         A18: y in D and

         A19: for z be Element of T st z in D & z >= y holds z in B by A14;

        consider z be Element of T such that

         A20: z in D and

         A21: x <= z and

         A22: y <= z by A16, A18, WAYBEL_0:def 1;

        take z;

        thus z in D by A20;

        let u be Element of T such that

         A23: u in D;

        assume

         A24: u >= z;

        then u >= x by A21, YELLOW_0:def 2;

        then

         A25: u in A by A17, A23;

        u >= y by A22, A24, YELLOW_0:def 2;

        then u in B by A19, A23;

        hence thesis by A25, XBOOLE_0:def 4;

      end;

      hence thesis by A1, A11, A13;

    end;

    begin

    reserve R for non empty RelStr,

N for net of R,

i for Element of N;

    definition

      let R, N;

      :: WAYBEL11:def6

      func lim_inf N -> Element of R equals ( "\/" ( the set of all ( "/\" ({ (N . i) : i >= j },R)) where j be Element of N,R));

      correctness ;

    end

    definition

      let R be reflexive non empty RelStr;

      let N be net of R, p be Element of R;

      :: WAYBEL11:def7

      pred p is_S-limit_of N means p <= ( lim_inf N);

    end

    definition

      let R be reflexive non empty RelStr;

      :: WAYBEL11:def8

      func Scott-Convergence R -> Convergence-Class of R means

      : Def8: for N be strict net of R st N in ( NetUniv R) holds for p be Element of R holds [N, p] in it iff p is_S-limit_of N;

      existence

      proof

        defpred P[ set, Element of R] means ex N be strict net of R st N = $1 & $2 is_S-limit_of N;

        consider C be Relation of ( NetUniv R), the carrier of R such that

         A1: for x be Element of ( NetUniv R), y be Element of R holds [x, y] in C iff P[x, y] from RELSET_1:sch 2;

        reconsider C as Convergence-Class of R by YELLOW_6:def 18;

        take C;

        let N be strict net of R such that

         A2: N in ( NetUniv R);

        let p be Element of R;

        hereby

          assume [N, p] in C;

          then ex M be strict net of R st M = N & p is_S-limit_of M by A1, A2;

          hence p is_S-limit_of N;

        end;

        thus thesis by A1, A2;

      end;

      uniqueness

      proof

        let it1,it2 be Convergence-Class of R such that

         A3: for N be strict net of R st N in ( NetUniv R) holds for p be Element of R holds [N, p] in it1 iff p is_S-limit_of N and

         A4: for N be strict net of R st N in ( NetUniv R) holds for p be Element of R holds [N, p] in it2 iff p is_S-limit_of N;

        let x,y be object;

        

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

        

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

        hereby

          assume

           A7: [x, y] in it1;

          then

           A8: x in ( NetUniv R) by A5, ZFMISC_1: 87;

          then

          consider N be strict net of R such that

           A9: N = x and the carrier of N in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

          reconsider p = y as Element of R by A5, A7, ZFMISC_1: 87;

          p is_S-limit_of N by A3, A7, A8, A9;

          hence [x, y] in it2 by A4, A8, A9;

        end;

        assume

         A10: [x, y] in it2;

        then

         A11: x in ( NetUniv R) by A6, ZFMISC_1: 87;

        then

        consider N be strict net of R such that

         A12: N = x and the carrier of N in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

        reconsider p = y as Element of R by A6, A10, ZFMISC_1: 87;

        p is_S-limit_of N by A4, A10, A11, A12;

        hence thesis by A3, A11, A12;

      end;

    end

    theorem :: WAYBEL11:17

    for R be complete LATTICE, N be net of R, p,q be Element of R st p is_S-limit_of N & N is_eventually_in ( downarrow q) holds p <= q

    proof

      let R be complete LATTICE, N be net of R, p,q be Element of R such that

       A1: p <= ( lim_inf N) and

       A2: N is_eventually_in ( downarrow q);

      consider j0 be Element of N such that

       A3: for i be Element of N st j0 <= i holds (N . i) in ( downarrow q) by A2;

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

      reconsider q9 = q as Element of R;

      q9 is_>=_than X

      proof

        let x be Element of R;

        assume x in X;

        then

        consider j1 be Element of N such that

         A4: x = ( "/\" ({ (N . i) where i be Element of N : i >= j1 },R));

        set Y = { (N . i) where i be Element of N : i >= j1 };

        reconsider j1 as Element of N;

        consider j2 be Element of N such that

         A5: j2 >= j0 and

         A6: j2 >= j1 by YELLOW_6:def 3;

        (N . j2) in Y by A6;

        then

         A7: x <= (N . j2) by A4, YELLOW_2: 22;

        (N . j2) in ( downarrow q) by A3, A5;

        then (N . j2) <= q9 by WAYBEL_0: 17;

        hence x <= q9 by A7, YELLOW_0:def 2;

      end;

      then ( lim_inf N) <= q9 by YELLOW_0: 32;

      hence thesis by A1, YELLOW_0:def 2;

    end;

    theorem :: WAYBEL11:18

    

     Th18: for R be complete LATTICE, N be net of R, p,q be Element of R st N is_eventually_in ( uparrow q) holds ( lim_inf N) >= q

    proof

      let R be complete LATTICE, N be net of R, p,q be Element of R;

      assume N is_eventually_in ( uparrow q);

      then

      consider j0 be Element of N such that

       A1: for i be Element of N st j0 <= i holds (N . i) in ( uparrow q);

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

      set Y = { (N . i) where i be Element of N : i >= j0 };

      reconsider q9 = q as Element of R;

      ( "/\" (Y,R)) in X;

      then

       A2: ( lim_inf N) >= ( "/\" (Y,R)) by YELLOW_2: 22;

      q9 is_<=_than Y

      proof

        let y be Element of R;

        assume y in Y;

        then

        consider i1 be Element of N such that

         A3: y = (N . i1) and

         A4: i1 >= j0;

        reconsider i19 = i1 as Element of N;

        (N . i19) in ( uparrow q) by A1, A4;

        hence q9 <= y by A3, WAYBEL_0: 18;

      end;

      then ( "/\" (Y,R)) >= q9 by YELLOW_0: 33;

      hence thesis by A2, YELLOW_0:def 2;

    end;

    definition

      let R be reflexive non empty RelStr, N be non empty NetStr over R;

      :: original: monotone

      redefine

      :: WAYBEL11:def9

      attr N is monotone means

      : Def9: for i,j be Element of N st i <= j holds (N . i) <= (N . j);

      compatibility

      proof

        hereby

          assume N is monotone;

          then

           A1: ( netmap (N,R)) is monotone;

          let i,j be Element of N;

          assume i <= j;

          hence (N . i) <= (N . j) by A1;

        end;

        assume

         A2: for i,j be Element of N st i <= j holds (N . i) <= (N . j);

        ( netmap (N,R)) is monotone

        proof

          let x,y be Element of N;

          

           A3: (( netmap (N,R)) . x) = (N . x);

          

           A4: (( netmap (N,R)) . y) = (N . y);

          assume x <= y;

          hence (( netmap (N,R)) . x) <= (( netmap (N,R)) . y) by A2, A3, A4;

        end;

        hence thesis;

      end;

    end

    definition

      let R be non empty RelStr;

      let S be non empty set, f be Function of S, the carrier of R;

      :: WAYBEL11:def10

      func Net-Str (S,f) -> strict non empty NetStr over R means

      : Def10: the carrier of it = S & the mapping of it = f & for i,j be Element of it holds i <= j iff (it . i) <= (it . j);

      existence

      proof

        defpred P[ Element of S, Element of S] means (f . $1) <= (f . $2);

        consider R be Relation of S, S such that

         A1: for x,y be Element of S holds [x, y] in R iff P[x, y] from RELSET_1:sch 2;

        take N = NetStr (# S, R, f #);

        thus the carrier of N = S;

        thus the mapping of N = f;

        let i,j be Element of N;

        reconsider x = i, y = j as Element of S;

         [x, y] in the InternalRel of N iff (f . x) <= (f . y) by A1;

        hence thesis by ORDERS_2:def 5;

      end;

      uniqueness

      proof

        let it1,it2 be strict non empty NetStr over R such that

         A2: the carrier of it1 = S and

         A3: the mapping of it1 = f and

         A4: for i,j be Element of it1 holds i <= j iff (it1 . i) <= (it1 . j) and

         A5: the carrier of it2 = S and

         A6: the mapping of it2 = f and

         A7: for i,j be Element of it2 holds i <= j iff (it2 . i) <= (it2 . j);

        the InternalRel of it1 = the InternalRel of it2

        proof

          let x,y be object;

          hereby

            assume

             A8: [x, y] in the InternalRel of it1;

            then

            reconsider i = x, j = y as Element of it1 by ZFMISC_1: 87;

            reconsider i9 = x, j9 = y as Element of it2 by A2, A5, A8, ZFMISC_1: 87;

            

             A9: (it1 . i) = (it2 . i9) by A3, A6;

            

             A10: (it1 . j) = (it2 . j9) by A3, A6;

            i <= j by A8, ORDERS_2:def 5;

            then (it2 . i9) <= (it2 . j9) by A4, A9, A10;

            then i9 <= j9 by A7;

            hence [x, y] in the InternalRel of it2 by ORDERS_2:def 5;

          end;

          assume

           A11: [x, y] in the InternalRel of it2;

          then

          reconsider i = x, j = y as Element of it2 by ZFMISC_1: 87;

          reconsider i9 = x, j9 = y as Element of it1 by A2, A5, A11, ZFMISC_1: 87;

          

           A12: (it2 . i) = (it1 . i9) by A3, A6;

          

           A13: (it2 . j) = (it1 . j9) by A3, A6;

          i <= j by A11, ORDERS_2:def 5;

          then (it1 . i9) <= (it1 . j9) by A7, A12, A13;

          then i9 <= j9 by A4;

          hence thesis by ORDERS_2:def 5;

        end;

        hence thesis by A2, A3, A5, A6;

      end;

    end

    theorem :: WAYBEL11:19

    

     Th19: for L be non empty 1-sorted, N be non empty NetStr over L holds ( rng the mapping of N) = the set of all (N . i) where i be Element of N

    proof

      let L be non empty 1-sorted, N be non empty NetStr over L;

      set X = the set of all (N . i) where i be Element of N;

      

       A1: the carrier of N = ( dom the mapping of N) by FUNCT_2:def 1;

      thus ( rng the mapping of N) c= the set of all (N . i) where i be Element of N

      proof

        let e be object;

        assume e in ( rng the mapping of N);

        then

        consider u be object such that

         A2: u in ( dom the mapping of N) and

         A3: e = (the mapping of N . u) by FUNCT_1:def 3;

        reconsider u as Element of N by A2;

        e = (N . u) by A3;

        hence thesis;

      end;

      let e be object;

      assume e in X;

      then ex i be Element of N st (e = (N . i));

      hence thesis by A1, FUNCT_1:def 3;

    end;

    theorem :: WAYBEL11:20

    

     Th20: for R be non empty RelStr, S be non empty set, f be Function of S, the carrier of R st ( rng f) is directed holds ( Net-Str (S,f)) is directed

    proof

      let R be non empty RelStr, S be non empty set, f be Function of S, the carrier of R such that

       A1: ( rng f) is directed;

      set N = ( Net-Str (S,f));

      let x,y be Element of N;

      f = the mapping of N by Def10;

      then

       A2: ( rng f) = the set of all (N . i) where i be Element of N by Th19;

      then

       A3: (N . x) in ( rng f);

      (N . y) in ( rng f) by A2;

      then

      consider p be Element of R such that

       A4: p in ( rng f) and

       A5: (N . x) <= p and

       A6: (N . y) <= p by A1, A3;

      consider z be object such that

       A7: z in ( dom f) and

       A8: p = (f . z) by A4, FUNCT_1:def 3;

      reconsider z as Element of N by A7, Def10;

      take z;

      p = (N . z) by A8, Def10;

      hence thesis by A5, A6, Def10;

    end;

    registration

      let R be non empty RelStr;

      let S be non empty set, f be Function of S, the carrier of R;

      cluster ( Net-Str (S,f)) -> monotone;

      coherence

      proof

        set N = ( Net-Str (S,f));

        ( netmap (N,R)) is monotone

        proof

          let x,y be Element of N;

          

           A1: (( netmap (N,R)) . x) = (N . x);

          

           A2: (( netmap (N,R)) . y) = (N . y);

          assume x <= y;

          hence (( netmap (N,R)) . x) <= (( netmap (N,R)) . y) by A1, A2, Def10;

        end;

        hence thesis;

      end;

    end

    registration

      let R be transitive non empty RelStr;

      let S be non empty set, f be Function of S, the carrier of R;

      cluster ( Net-Str (S,f)) -> transitive;

      coherence

      proof

        set N = ( Net-Str (S,f));

        let x,y,z be Element of N;

        assume that

         A1: x <= y and

         A2: y <= z;

        

         A3: (N . x) <= (N . y) by A1, Def10;

        (N . y) <= (N . z) by A2, Def10;

        then (N . x) <= (N . z) by A3, YELLOW_0:def 2;

        hence thesis by Def10;

      end;

    end

    registration

      let R be reflexive non empty RelStr;

      let S be non empty set, f be Function of S, the carrier of R;

      cluster ( Net-Str (S,f)) -> reflexive;

      coherence

      proof

        let x be Element of ( Net-Str (S,f));

        (( Net-Str (S,f)) . x) <= (( Net-Str (S,f)) . x);

        hence thesis by Def10;

      end;

    end

    theorem :: WAYBEL11:21

    

     Th21: for R be non empty transitive RelStr, S be non empty set, f be Function of S, the carrier of R st S c= the carrier of R & ( Net-Str (S,f)) is directed holds ( Net-Str (S,f)) in ( NetUniv R)

    proof

      let R be non empty transitive RelStr, S be non empty set, f be Function of S, the carrier of R such that

       A1: S c= the carrier of R and

       A2: ( Net-Str (S,f)) is directed;

      reconsider N = ( Net-Str (S,f)) as strict net of R by A2;

      set UN = ( the_universe_of the carrier of R);

      reconsider UN as universal set;

      ( the_transitive-closure_of the carrier of R) in UN by CLASSES1: 2;

      then the carrier of R in UN by CLASSES1: 3, CLASSES1: 52;

      then

       A3: S in UN by A1, CLASSES1:def 1;

      the carrier of N = S by Def10;

      hence thesis by A3, YELLOW_6:def 11;

    end;

    registration

      let R be LATTICE;

      cluster monotone reflexive strict for net of R;

      existence

      proof

        reconsider f = ( id the carrier of R) as Function of the carrier of R, the carrier of R;

        ( rng f) = ( [#] R) by RELAT_1: 45;

        then

        reconsider N = ( Net-Str (the carrier of R,f)) as strict reflexive net of R by Th20;

        take N;

        thus thesis;

      end;

    end

    defpred P[ set] means not contradiction;

    theorem :: WAYBEL11:22

    

     Th22: for R be complete LATTICE, N be monotone reflexive net of R holds ( lim_inf N) = ( sup N)

    proof

      let R be complete LATTICE, N be monotone reflexive net of R;

      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] };

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

      

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

      proof

        let j be Element of N;

        set Y = { (N . i) where i be Element of N : i >= j };

        

         A2: (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 Def9;

        end;

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

        proof

          let b be Element of R;

          assume

           A3: b is_<=_than Y;

          reconsider j9 = j as Element of N;

          j9 <= j9;

          then (N . j9) in Y;

          hence thesis by A3;

        end;

        hence thesis by A2, YELLOW_0: 33;

      end;

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

      .= 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 :: WAYBEL11:23

    

     Th23: for R be complete LATTICE, N be constant net of R holds ( the_value_of N) = ( lim_inf N)

    proof

      let R be complete LATTICE, N be constant net of R;

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

      set j = the Element of N;

      

       A1: (N . j) is_>=_than X

      proof

        let b be Element of R;

        assume b in X;

        then

        consider j0 be Element of N such that

         A2: b = ( "/\" ({ (N . i) where i be Element of N : i >= j0 },R));

        reconsider j0 as Element of N;

        consider i0 be Element of N such that

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

        

         A4: (N . i0) in { (N . i) where i be Element of N : i >= j0 } by A3;

        (N . i0) = ( the_value_of N) by YELLOW_6: 16

        .= (N . j) by YELLOW_6: 16;

        hence thesis by A2, A4, YELLOW_2: 22;

      end;

      

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

      proof

        let b be Element of R;

        set Y = { (N . i) where i be Element of N : i >= j };

        

         A6: ( "/\" (Y,R)) in X;

        assume b is_>=_than X;

        then

         A7: b >= ( "/\" (Y,R)) by A6;

        

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

        proof

          let c be Element of R;

          assume c in Y;

          then

          consider i0 be Element of N such that

           A9: c = (N . i0) and i0 >= j;

          (N . j) = ( the_value_of N) by YELLOW_6: 16

          .= (N . i0) by YELLOW_6: 16;

          hence (N . j) <= c by A9;

        end;

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

        proof

          let c be Element of R;

          consider i0 be Element of N such that

           A10: i0 >= j and i0 >= j by YELLOW_6:def 3;

          

           A11: (N . i0) in Y by A10;

          assume

           A12: c is_<=_than Y;

          (N . j) = ( the_value_of N) by YELLOW_6: 16

          .= (N . i0) by YELLOW_6: 16;

          hence thesis by A11, A12;

        end;

        hence thesis by A7, A8, YELLOW_0: 33;

      end;

      

      thus ( the_value_of N) = (N . j) by YELLOW_6: 16

      .= ( lim_inf N) by A1, A5, YELLOW_0: 32;

    end;

    theorem :: WAYBEL11:24

    

     Th24: for R be complete LATTICE, N be constant net of R holds ( the_value_of N) is_S-limit_of N by Th23;

    definition

      let S be non empty 1-sorted, e be Element of S;

      :: WAYBEL11:def11

      func Net-Str e -> strict NetStr over S means

      : Def11: the carrier of it = {e} & the InternalRel of it = { [e, e]} & the mapping of it = ( id {e});

      existence

      proof

        e in {e} by TARSKI:def 1;

        then

        reconsider r = { [e, e]} as Relation of {e} by RELSET_1: 3;

        

         A1: ( dom ( id {e})) = {e} by RELAT_1: 45;

        ( rng ( id {e})) = {e} by RELAT_1: 45;

        then

        reconsider f = ( id {e}) as Function of {e}, the carrier of S by A1, RELSET_1: 4;

        take NetStr (# {e}, r, f #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let S be non empty 1-sorted, e be Element of S;

      cluster ( Net-Str e) -> non empty;

      coherence

      proof

        set N = ( Net-Str e);

        the carrier of N = {e} by Def11;

        hence the carrier of N is non empty;

      end;

    end

    theorem :: WAYBEL11:25

    

     Th25: for S be non empty 1-sorted, e be Element of S, x be Element of ( Net-Str e) holds x = e

    proof

      let S be non empty 1-sorted, e be Element of S, x be Element of ( Net-Str e);

      the carrier of ( Net-Str e) = {e} by Def11;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: WAYBEL11:26

    

     Th26: for S be non empty 1-sorted, e be Element of S, x be Element of ( Net-Str e) holds (( Net-Str e) . x) = e

    proof

      let S be non empty 1-sorted, e be Element of S, x be Element of ( Net-Str e);

      set N = ( Net-Str e);

      

       A1: the carrier of ( Net-Str e) = {e} by Def11;

      then

       A2: x = e by TARSKI:def 1;

      

      thus (N . x) = (( id {e}) . x) by Def11

      .= e by A1, A2;

    end;

    registration

      let S be non empty 1-sorted, e be Element of S;

      cluster ( Net-Str e) -> reflexive transitive directed antisymmetric;

      coherence

      proof

        set N = ( Net-Str e);

        the carrier of N = {e} by Def11;

        then

        reconsider e as Element of N by TARSKI:def 1;

        the InternalRel of N = { [e, e]} by Def11;

        then

         A1: [e, e] in the InternalRel of N by TARSKI:def 1;

        thus N is reflexive

        proof

          let x be Element of N;

          x = e by Th25;

          hence thesis by A1, ORDERS_2:def 5;

        end;

        thus N is transitive

        proof

          let x,y,z be Element of N such that x <= y and y <= z;

          

           A2: x = e by Th25;

          z = e by Th25;

          hence thesis by A1, A2, ORDERS_2:def 5;

        end;

        thus N is directed

        proof

          let x,y be Element of N;

          take e;

          

           A3: x = e by Th25;

          y = e by Th25;

          hence thesis by A1, A3, ORDERS_2:def 5;

        end;

        let x,y be Element of N such that x <= y and y <= x;

        x = e by Th25;

        hence thesis by Th25;

      end;

    end

    theorem :: WAYBEL11:27

    

     Th27: for S be non empty 1-sorted, e be Element of S, X be set holds ( Net-Str e) is_eventually_in X iff e in X

    proof

      let S be non empty 1-sorted, e be Element of S, X be set;

      set N = ( Net-Str e);

      the carrier of N = {e} by Def11;

      then

      reconsider d = e as Element of N by TARSKI:def 1;

      hereby

        assume N is_eventually_in X;

        then

        consider x be Element of N such that

         A1: for y be Element of N st x <= y holds (N . y) in X;

        (N . x) in X by A1;

        hence e in X by Th26;

      end;

      assume

       A2: e in X;

      take d;

      let j be Element of N such that d <= j;

      thus thesis by A2, Th26;

    end;

    theorem :: WAYBEL11:28

    

     Th28: for S be reflexive antisymmetric non empty RelStr, e be Element of S holds e = ( lim_inf ( Net-Str e))

    proof

      let S be reflexive antisymmetric non empty RelStr, e be Element of S;

      set N = ( Net-Str e), X = the set of all ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) where j be Element of N;

      reconsider e9 = e as Element of S;

      

       A1: X c= {e9}

      proof

        let u be object;

        assume u in X;

        then

        consider j be Element of N such that

         A2: u = ( "/\" ({ (N . i) where i be Element of N : i >= j },S));

        set Y = { (N . i) where i be Element of N : i >= j };

        

         A3: Y c= {e9}

        proof

          let v be object;

          assume v in Y;

          then

          consider i be Element of N such that

           A4: v = (N . i) and i >= j;

          reconsider i9 = i as Element of N;

          (N . i9) = e by Th26;

          hence thesis by A4, TARSKI:def 1;

        end;

        reconsider j9 = j as Element of N;

        j9 <= j9;

        then (N . j) in Y;

        then Y = {e9} by A3, ZFMISC_1: 33;

        then u = e9 by A2, YELLOW_0: 39;

        hence thesis by TARSKI:def 1;

      end;

      set j = the Element of N;

      ( "/\" ({ (N . i) where i be Element of N : i >= j },S)) in X;

      then X = {e9} by A1, ZFMISC_1: 33;

      hence thesis by YELLOW_0: 39;

    end;

    theorem :: WAYBEL11:29

    

     Th29: for S be non empty reflexive RelStr, e be Element of S holds ( Net-Str e) in ( NetUniv S)

    proof

      let S be non empty reflexive RelStr, e be Element of S;

      set N = ( Net-Str e), UN = ( the_universe_of the carrier of S);

      

       A1: the carrier of N = {e} by Def11;

      reconsider UN as universal set;

      ( the_transitive-closure_of the carrier of S) in UN by CLASSES1: 2;

      then the carrier of S in UN by CLASSES1: 3, CLASSES1: 52;

      then the carrier of N in ( the_universe_of the carrier of S) by A1, CLASSES1:def 1;

      hence thesis by YELLOW_6:def 11;

    end;

    theorem :: WAYBEL11:30

    

     Th30: for R be complete LATTICE, 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 LATTICE, 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;

      set E1 = { (Z . k) where k be Element of Z : k >= jx }, Ey = { (Z . k) where k be Element of Z : k >= jy }, E = { (Z . k) where k be Element of Z : k >= j };

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

      thus z in D by A1;

      E c= E1

      proof

        let e be object;

        assume e in E;

        then

        consider k be Element of Z such that

         A6: e = (Z . k) and

         A7: k >= j;

        reconsider k as Element of Z;

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

        hence thesis by A6;

      end;

      hence x <= z by A2, WAYBEL_7: 1;

      E c= Ey

      proof

        let e be object;

        assume e in E;

        then

        consider k be Element of Z such that

         A8: e = (Z . k) and

         A9: k >= j;

        reconsider k as Element of Z;

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

        hence thesis by A8;

      end;

      hence y <= z by A3, WAYBEL_7: 1;

    end;

    theorem :: WAYBEL11:31

    

     Th31: for L be complete LATTICE holds for S be Subset of L holds S in the topology of ( ConvergenceSpace ( Scott-Convergence L)) iff S is inaccessible upper

    proof

      let L be complete LATTICE;

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

      

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

      let S be Subset of L;

      hereby

        assume S in the topology of T;

        then

         A2: ex V be Subset of L st (S = V) & (for p be Element of L st p in V holds for N be net of L 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 L 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 L by A4, RELSET_1: 4;

          reconsider N = ( Net-Str (D,f)) as strict monotone reflexive net of L by A5, Th20;

          

           A6: N in ( NetUniv L) by Th21;

          ( lim_inf N) = ( sup N) by Th22

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

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

          .= ( "\/" (( rng f),L)) by Def10

          .= ( sup D) by RELAT_1: 45;

          then ( sup D) is_S-limit_of N;

          then [N, ( sup D)] in SC by A6, Def8;

          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 Def10;

          (N . j0) = (( id D) . j0) by Def10

          .= j0 by A10;

          hence thesis by A9, A10, XBOOLE_0: 3;

        end;

        thus S is upper

        proof

          let x,y be Element of L such that

           A11: x in S and

           A12: x <= y;

          

           A13: ( Net-Str y) in ( NetUniv L) by Th29;

          y = ( lim_inf ( Net-Str y)) by Th28;

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

          then [( Net-Str y), x] in SC by A13, Def8;

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

          hence thesis by Th27;

        end;

      end;

      assume that

       A14: S is inaccessible and

       A15: S is upper;

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

      proof

        let p be Element of L such that

         A16: p in S;

        reconsider p9 = p as Element of L;

        let N be net of L;

        assume

         A17: [N, p] in SC;

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

        then

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

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

        then p is_S-limit_of N by A17, A18, Def8;

        then

         A19: p9 <= ( lim_inf N);

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

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

        X is Subset of L from DOMAIN_1:sch 8;

        then

        reconsider D = X as Subset of L;

        reconsider D as non empty directed Subset of L by Th30;

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

        then D meets S by A14;

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

        then

        consider d be Element of L such that

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

        reconsider d as Element of L;

        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 },L));

        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 { (N . i) where i be Element of N : i >= j };

        then d <= (N . i0) by A21, YELLOW_2: 22;

        hence thesis by A15, A22;

      end;

      hence thesis by A1;

    end;

    theorem :: WAYBEL11:32

    

     Th32: for T be complete Scott TopLattice holds the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence T))

    proof

      let T be complete Scott TopLattice;

      set CSC = ( ConvergenceSpace ( Scott-Convergence T));

      the topology of T = the topology of CSC

      proof

        thus the topology of T c= the topology of CSC

        proof

          let e be object;

          assume

           A1: e in the topology of T;

          then

          reconsider A = e as Subset of T;

          A is open by A1;

          then A is inaccessible upper by Def4;

          hence thesis by Th31;

        end;

        let e be object;

        assume

         A2: e in the topology of CSC;

        then

        reconsider A = e as Subset of T by YELLOW_6:def 24;

        A is inaccessible upper by A2, Th31;

        then A is open by Def4;

        hence thesis;

      end;

      hence thesis by YELLOW_6:def 24;

    end;

    theorem :: WAYBEL11:33

    

     Th33: for T be complete TopLattice st the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence T)) holds for S be Subset of T holds S is open iff S is inaccessible upper

    proof

      let T be complete TopLattice;

      set SC = ( Scott-Convergence T);

      assume the TopStruct of T = ( ConvergenceSpace SC);

      then

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

      let S be Subset of T;

      hereby

        assume S is open;

        then S in the topology of T;

        then

         A2: ex V be Subset of T st (S = V) & (for p be Element of T st p in V holds for N be net of T 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 T 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 T by A4, RELSET_1: 4;

          reconsider N = ( Net-Str (D,f)) as strict monotone reflexive net of T by A5, Th20;

          

           A6: N in ( NetUniv T) by Th21;

          ( lim_inf N) = ( sup N) by Th22

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

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

          .= ( "\/" (( rng f),T)) by Def10

          .= ( sup D) by RELAT_1: 45;

          then ( sup D) is_S-limit_of N;

          then [N, ( sup D)] in SC by A6, Def8;

          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 Def10;

          (N . j0) = (( id D) . j0) by Def10

          .= j0 by A10;

          hence thesis by A9, A10, XBOOLE_0: 3;

        end;

        thus S is upper

        proof

          let x,y be Element of T such that

           A11: x in S and

           A12: x <= y;

          

           A13: ( Net-Str y) in ( NetUniv T) by Th29;

          y = ( lim_inf ( Net-Str y)) by Th28;

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

          then [( Net-Str y), x] in SC by A13, Def8;

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

          hence thesis by Th27;

        end;

      end;

      assume that

       A14: S is inaccessible and

       A15: S is upper;

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

      proof

        let p be Element of T such that

         A16: p in S;

        reconsider p9 = p as Element of T;

        let N be net of T;

        assume

         A17: [N, p] in SC;

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

        then

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

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

        then p is_S-limit_of N by A17, A18, Def8;

        then

         A19: p9 <= ( lim_inf N);

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

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

        X is Subset of T from DOMAIN_1:sch 8;

        then

        reconsider D = X as Subset of T;

        reconsider D as non empty directed Subset of T by Th30;

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

        then D meets S by A14;

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

        then

        consider d be Element of T such that

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

        reconsider d as Element of T;

        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 },T));

        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 { (N . i) where i be Element of N : i >= j };

        then d <= (N . i0) by A21, YELLOW_2: 22;

        hence thesis by A15, A22;

      end;

      then S in the topology of T by A1;

      hence thesis;

    end;

    theorem :: WAYBEL11:34

    

     Th34: for T be complete TopLattice st the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence T)) holds T is Scott by Th33;

    registration

      let R be complete LATTICE;

      cluster ( Scott-Convergence R) -> (CONSTANTS);

      coherence

      proof

        let N be constant net of R;

        assume

         A1: N in ( NetUniv R);

        then

        consider M be strict net of R such that

         A2: M = N and the carrier of M in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

        ( the_value_of M) is_S-limit_of M by A2, Th24;

        hence thesis by A1, A2, Def8;

      end;

    end

    registration

      let R be complete LATTICE;

      cluster ( Scott-Convergence R) -> (SUBNETS);

      coherence

      proof

        set S = ( Scott-Convergence R);

        let N be net of R, Y be subnet of N;

        

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

        assume

         A2: Y in ( NetUniv R);

        then

        consider Y9 be strict net of R such that

         A3: Y9 = Y and the carrier of Y9 in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

        let p be Element of R;

        assume

         A4: [N, p] in S;

        then

         A5: N in ( NetUniv R) by A1, ZFMISC_1: 87;

        then

        consider N9 be strict net of R such that

         A6: N9 = N and the carrier of N9 in ( the_universe_of the carrier of R) by YELLOW_6:def 11;

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

        reconsider X1 = { F(j) where j be Element of N : P[j] } as Subset of R from DOMAIN_1:sch 8;

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

        reconsider X2 = { G(j) where j be Element of Y : P[j] } as Subset of R from DOMAIN_1:sch 8;

        p is_S-limit_of N9 by A4, A5, A6, Def8;

        then

         A7: p <= ( lim_inf N) by A6;

        consider f be Function of Y, N such that

         A8: the mapping of Y = (the mapping of N * f) and

         A9: for m be Element of N holds ex n be Element of Y st for p be Element of Y st n <= p holds m <= (f . p) by YELLOW_6:def 9;

        X1 is_finer_than X2

        proof

          let a be Element of R;

          assume a in X1;

          then

          consider j be Element of N such that

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

          reconsider j as Element of N;

          consider n be Element of Y such that

           A11: for p be Element of Y st n <= p holds j <= (f . p) by A9;

          set X3 = { (Y . i) where i be Element of Y : i >= n }, X4 = { (N . i) where i be Element of N : i >= j };

          take b = ( "/\" (X3,R));

          thus b in X2;

          X3 c= X4

          proof

            let u be object;

            assume u in X3;

            then

            consider m be Element of Y such that

             A12: u = (Y . m) and

             A13: m >= n;

            reconsider m as Element of Y;

            

             A14: (f . m) >= j by A11, A13;

            u = (N . (f . m)) by A8, A12, FUNCT_2: 15;

            hence thesis by A14;

          end;

          hence a <= b by A10, WAYBEL_7: 1;

        end;

        then ( "\/" (X1,R)) <= ( "\/" (X2,R)) by Th2;

        then p <= ( lim_inf Y) by A7, YELLOW_0:def 2;

        then p is_S-limit_of Y9 by A3;

        hence thesis by A2, A3, Def8;

      end;

    end

    theorem :: WAYBEL11:35

    

     Th35: for S be non empty 1-sorted, N be net of S, X be set holds for M be subnet of N st M = (N " X) holds for i be Element of M holds (M . i) in X

    proof

      let S be non empty 1-sorted, N be net of S, X be set;

      let M be subnet of N such that

       A1: M = (N " X);

      let j be Element of M;

      j in the carrier of M;

      then j in (the mapping of N " X) by A1, YELLOW_6:def 10;

      then

       A2: (the mapping of N . j) in X by FUNCT_1:def 7;

      the mapping of M = (the mapping of N | the carrier of M) by A1, YELLOW_6:def 6;

      hence thesis by A2, FUNCT_1: 49;

    end;

    definition

      let L be non empty reflexive RelStr;

      :: WAYBEL11:def12

      func sigma L -> Subset-Family of L equals the topology of ( ConvergenceSpace ( Scott-Convergence L));

      coherence by YELLOW_6:def 24;

    end

    theorem :: WAYBEL11:36

    

     Th36: for L be continuous complete Scott TopLattice, x be Element of L holds ( wayabove x) is open

    proof

      let L be continuous complete Scott TopLattice, x be Element of L;

      set W = ( wayabove x);

      W is inaccessible

      proof

        let D be non empty directed Subset of L;

        assume ( sup D) in W;

        then x << ( sup D) by WAYBEL_3: 8;

        then

        consider d be Element of L such that

         A1: d in D and

         A2: x << d by WAYBEL_4: 53;

        d in W by A2;

        hence thesis by A1, XBOOLE_0: 3;

      end;

      hence thesis by Def4;

    end;

    theorem :: WAYBEL11:37

    

     Th37: for T be complete TopLattice st the topology of T = ( sigma T) holds T is Scott

    proof

      let T be complete TopLattice;

      set CSC = ( ConvergenceSpace ( Scott-Convergence T));

      assume the topology of T = ( sigma T);

      then the TopStruct of T = TopStruct (# the carrier of CSC, the topology of CSC #) by YELLOW_6:def 24;

      hence thesis by Th34;

    end;

    

     Lm3: for T1,T2 be TopStruct st the TopStruct of T1 = the TopStruct of T2 & T1 is TopSpace-like holds T2 is TopSpace-like;

    

     Lm4: for S1,S2 be non empty 1-sorted st the carrier of S1 = the carrier of S2 holds for N be strict net of S1 holds N is strict net of S2;

    

     Lm5: for S1,S2 be non empty 1-sorted st the carrier of S1 = the carrier of S2 holds ( NetUniv S1) = ( NetUniv S2)

    proof

      let S1,S2 be non empty 1-sorted;

      assume

       A1: the carrier of S1 = the carrier of S2;

      defpred P[ set] means ex N be strict net of S2 st N = $1 & the carrier of N in ( the_universe_of the carrier of S2);

       A2:

      now

        let x be set;

        hereby

          assume x in ( NetUniv S1);

          then

          consider N be strict net of S1 such that

           A3: N = x and

           A4: the carrier of N in ( the_universe_of the carrier of S1) by YELLOW_6:def 11;

          reconsider N as strict net of S2 by A1;

          thus P[x]

          proof

            take N;

            thus thesis by A1, A3, A4;

          end;

        end;

        assume P[x];

        then

        consider N be strict net of S2 such that

         A5: N = x and

         A6: the carrier of N in ( the_universe_of the carrier of S2);

        reconsider N as strict net of S1 by A1;

        now

          take N;

          thus N = x & the carrier of N in ( the_universe_of the carrier of S1) by A1, A5, A6;

        end;

        hence x in ( NetUniv S1) by YELLOW_6:def 11;

      end;

      

       A7: for x be set holds x in ( NetUniv S2) iff P[x] by YELLOW_6:def 11;

      thus ( NetUniv S1) = ( NetUniv S2) from XFAMILY:sch 2( A2, A7);

    end;

    

     Lm6: for T1,T2 be non empty 1-sorted, X be set holds for N1 be net of T1, N2 be net of T2 st N1 = N2 & N1 is_eventually_in X holds N2 is_eventually_in X

    proof

      let T1,T2 be non empty 1-sorted, X be set;

      let N1 be net of T1, N2 be net of T2 such that

       A1: N1 = N2;

      assume N1 is_eventually_in X;

      then

      consider i be Element of N1 such that

       A2: for j be Element of N1 st i <= j holds (N1 . j) in X;

      reconsider ii = i as Element of N2 by A1;

      take ii;

      let jj be Element of N2;

      reconsider j = jj as Element of N1 by A1;

      assume

       A3: ii <= jj;

      (N2 . jj) = (N1 . j) by A1;

      hence thesis by A1, A2, A3;

    end;

    

     Lm7: for T1,T2 be non empty TopSpace st the TopStruct of T1 = the TopStruct of T2 holds for N1 be net of T1, N2 be net of T2 st N1 = N2 holds for p1 be Point of T1, p2 be Point of T2 st p1 = p2 & p1 in ( Lim N1) holds p2 in ( Lim N2)

    proof

      let T1,T2 be non empty TopSpace such that

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

      let N1 be net of T1, N2 be net of T2 such that

       A2: N1 = N2;

      let p1 be Point of T1, p2 be Point of T2 such that

       A3: p1 = p2 and

       A4: p1 in ( Lim N1);

      for V be a_neighborhood of p2 holds N2 is_eventually_in V

      proof

        let V be a_neighborhood of p2;

        reconsider W = V as Subset of T1 by A1;

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

        then

        consider G be Subset of T2 such that

         A5: G is open and

         A6: G c= V and

         A7: p2 in G by TOPS_1: 22;

        reconsider H = G as Subset of T1 by A1;

        G in the topology of T2 by A5;

        then H is open by A1;

        then p1 in ( Int W) by A3, A6, A7, TOPS_1: 22;

        then

        reconsider W = V as a_neighborhood of p1 by CONNSP_2:def 1;

        thus N2 is_eventually_in V

        proof

          N1 is_eventually_in W by A4, YELLOW_6:def 15;

          then

          consider i be Element of N1 such that

           A8: for j be Element of N1 st i <= j holds (N1 . j) in W;

          reconsider ii = i as Element of N2 by A2;

          take ii;

          let jj be Element of N2;

          reconsider j = jj as Element of N1 by A2;

          assume

           A9: ii <= jj;

          (N2 . jj) = (N1 . j) by A2;

          hence thesis by A2, A8, A9;

        end;

      end;

      hence thesis by YELLOW_6:def 15;

    end;

    

     Lm8: for T1,T2 be non empty TopSpace st the TopStruct of T1 = the TopStruct of T2 holds ( Convergence T1) = ( Convergence T2)

    proof

      let T1,T2 be non empty TopSpace such that

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

      

       A2: ( Convergence T1) c= [:( NetUniv T1), the carrier of T1:] by YELLOW_6:def 18;

      

       A3: ( Convergence T2) c= [:( NetUniv T2), the carrier of T2:] by YELLOW_6:def 18;

      let u1,u2 be object;

      hereby

        assume

         A4: [u1, u2] in ( Convergence T1);

        then

        consider N1 be Element of ( NetUniv T1), p1 be Point of T1 such that

         A5: [u1, u2] = [N1, p1] by A2, DOMAIN_1: 1;

        

         A6: N1 in ( NetUniv T1);

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

        then

        reconsider N1 as net of T1;

        

         A7: p1 in ( Lim N1) by A4, A5, YELLOW_6:def 19;

        reconsider N2 = N1 as net of T2 by A1;

        reconsider p2 = p1 as Point of T2 by A1;

        

         A8: N2 in ( NetUniv T2) by A1, A6, Lm5;

        p2 in ( Lim N2) by A1, A7, Lm7;

        hence [u1, u2] in ( Convergence T2) by A5, A8, YELLOW_6:def 19;

      end;

      assume

       A9: [u1, u2] in ( Convergence T2);

      then

      consider N1 be Element of ( NetUniv T2), p1 be Point of T2 such that

       A10: [u1, u2] = [N1, p1] by A3, DOMAIN_1: 1;

      

       A11: N1 in ( NetUniv T2);

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

      then

      reconsider N1 as net of T2;

      

       A12: p1 in ( Lim N1) by A9, A10, YELLOW_6:def 19;

      reconsider N2 = N1 as net of T1 by A1;

      reconsider p2 = p1 as Point of T1 by A1;

      

       A13: N2 in ( NetUniv T1) by A1, A11, Lm5;

      p2 in ( Lim N2) by A1, A12, Lm7;

      hence thesis by A10, A13, YELLOW_6:def 19;

    end;

    

     Lm9: for R1,R2 be non empty RelStr st the RelStr of R1 = the RelStr of R2 & R1 is LATTICE holds R2 is LATTICE

    proof

      let R1,R2 be non empty RelStr such that

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

       A2: R1 is LATTICE;

      

       A3: R2 is with_infima

      proof

        let x,y be Element of R2;

        reconsider x9 = x, y9 = y as Element of R1 by A1;

        consider z9 be Element of R1 such that

         A4: z9 <= x9 and

         A5: z9 <= y9 and

         A6: for w9 be Element of R1 st w9 <= x9 & w9 <= y9 holds w9 <= z9 by A2, LATTICE3:def 11;

        reconsider z = z9 as Element of R2 by A1;

        take z;

        thus z <= x & z <= y by A1, A4, A5, Lm1;

        let w be Element of R2;

        reconsider w9 = w as Element of R1 by A1;

        assume that

         A7: w <= x and

         A8: w <= y;

        

         A9: w9 <= x9 by A1, A7, Lm1;

        w9 <= y9 by A1, A8, Lm1;

        then w9 <= z9 by A6, A9;

        hence thesis by A1, Lm1;

      end;

      

       A10: R2 is with_suprema

      proof

        let x,y be Element of R2;

        reconsider x9 = x, y9 = y as Element of R1 by A1;

        consider z9 be Element of R1 such that

         A11: z9 >= x9 and

         A12: z9 >= y9 and

         A13: for w9 be Element of R1 st w9 >= x9 & w9 >= y9 holds w9 >= z9 by A2, LATTICE3:def 10;

        reconsider z = z9 as Element of R2 by A1;

        take z;

        thus z >= x & z >= y by A1, A11, A12, Lm1;

        let w be Element of R2;

        reconsider w9 = w as Element of R1 by A1;

        assume that

         A14: w >= x and

         A15: w >= y;

        

         A16: w9 >= x9 by A1, A14, Lm1;

        w9 >= y9 by A1, A15, Lm1;

        then w9 >= z9 by A13, A16;

        hence thesis by A1, Lm1;

      end;

      

       A17: R2 is reflexive by A1, A2, YELLOW_0:def 1, Lm1;

      

       A18: R2 is transitive

      proof

        let x,y,z be Element of R2;

        reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1;

        assume that

         A19: x <= y and

         A20: y <= z;

        

         A21: x9 <= y9 by A1, A19, Lm1;

        y9 <= z9 by A1, A20, Lm1;

        then x9 <= z9 by A2, A21, YELLOW_0:def 2;

        hence thesis by A1, Lm1;

      end;

      R2 is antisymmetric

      proof

        let x,y be Element of R2;

        reconsider x9 = x, y9 = y as Element of R1 by A1;

        assume that

         A22: x <= y and

         A23: y <= x;

        

         A24: x9 <= y9 by A1, A22, Lm1;

        y9 <= x9 by A1, A23, Lm1;

        hence thesis by A2, A24, YELLOW_0:def 3;

      end;

      hence thesis by A3, A10, A17, A18;

    end;

    

     Lm10: for R1,R2 be LATTICE, X be set st the RelStr of R1 = the RelStr of R2 holds for p1 be Element of R1, p2 be Element of R2 st p1 = p2 & X is_<=_than p1 holds X is_<=_than p2 by Lm1;

    

     Lm11: for R1,R2 be LATTICE, X be set st the RelStr of R1 = the RelStr of R2 holds for p1 be Element of R1, p2 be Element of R2 st p1 = p2 & X is_>=_than p1 holds X is_>=_than p2 by Lm1;

    

     Lm12: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds for D be set holds ( "\/" (D,R1)) = ( "\/" (D,R2))

    proof

      let R1,R2 be complete LATTICE such that

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

      let D be set;

      reconsider b = ( "\/" (D,R1)) as Element of R2 by A1;

      

       A2: ex_sup_of (D,R2) by YELLOW_0: 17;

      

       A3: ex_sup_of (D,R1) by YELLOW_0: 17;

      then D is_<=_than ( "\/" (D,R1)) by YELLOW_0:def 9;

      then

       A4: D is_<=_than b by A1, Lm10;

      for a be Element of R2 st D is_<=_than a holds a >= b

      proof

        let a be Element of R2;

        reconsider a9 = a as Element of R1 by A1;

        assume D is_<=_than a;

        then D is_<=_than a9 by A1, Lm10;

        then a9 >= ( "\/" (D,R1)) by A3, YELLOW_0:def 9;

        hence thesis by A1, Lm1;

      end;

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

    end;

    

     Lm13: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds for D be set holds ( "/\" (D,R1)) = ( "/\" (D,R2))

    proof

      let R1,R2 be complete LATTICE such that

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

      let D be set;

      reconsider b = ( "/\" (D,R1)) as Element of R2 by A1;

      

       A2: ex_inf_of (D,R2) by YELLOW_0: 17;

      

       A3: ex_inf_of (D,R1) by YELLOW_0: 17;

      then D is_>=_than ( "/\" (D,R1)) by YELLOW_0:def 10;

      then

       A4: D is_>=_than b by A1, Lm11;

      for a be Element of R2 st D is_>=_than a holds a <= b

      proof

        let a be Element of R2;

        reconsider a9 = a as Element of R1 by A1;

        assume D is_>=_than a;

        then D is_>=_than a9 by A1, Lm11;

        then a9 <= ( "/\" (D,R1)) by A3, YELLOW_0:def 10;

        hence thesis by A1, Lm1;

      end;

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

    end;

    

     Lm14: for R1,R2 be non empty reflexive RelStr st the RelStr of R1 = the RelStr of R2 holds for D be Subset of R1, D9 be Subset of R2 st D = D9 & D is directed holds D9 is directed

    proof

      let R1,R2 be non empty reflexive RelStr such that

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

      let D be Subset of R1, D9 be Subset of R2 such that

       A2: D = D9 and

       A3: D is directed;

      let x2,y2 be Element of R2 such that

       A4: x2 in D9 and

       A5: y2 in D9;

      reconsider x1 = x2, y1 = y2 as Element of R1 by A1;

      consider z1 be Element of R1 such that

       A6: z1 in D and

       A7: x1 <= z1 and

       A8: y1 <= z1 by A2, A3, A4, A5;

      reconsider z2 = z1 as Element of R2 by A1;

      take z2;

      thus z2 in D9 by A2, A6;

      thus x2 <= z2 & y2 <= z2 by A1, A7, A8, Lm1;

    end;

    

     Lm15: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds for p,q be Element of R1 st p << q holds for p9,q9 be Element of R2 st p = p9 & q = q9 holds p9 << q9

    proof

      let R1,R2 be complete LATTICE such that

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

      let p,q be Element of R1 such that

       A2: p << q;

      let p9,q9 be Element of R2 such that

       A3: p = p9 and

       A4: q = q9;

      let D9 be non empty directed Subset of R2 such that

       A5: q9 <= ( sup D9);

      reconsider D = D9 as non empty Subset of R1 by A1;

      reconsider D as non empty directed Subset of R1 by A1, Lm14;

      ( sup D) = ( sup D9) by A1, Lm12;

      then q <= ( sup D) by A1, A4, A5, Lm1;

      then

      consider d be Element of R1 such that

       A6: d in D and

       A7: p <= d by A2;

      reconsider d9 = d as Element of R2 by A1;

      take d9;

      thus d9 in D9 by A6;

      thus thesis by A1, A3, A7, Lm1;

    end;

    

     Lm16: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds for N1 be net of R1, N2 be net of R2 st N1 = N2 holds ( lim_inf N1) = ( lim_inf N2)

    proof

      let R1,R2 be complete LATTICE such that

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

      let N1 be net of R1, N2 be net of R2 such that

       A2: N1 = N2;

      set X1 = the set of all ( "/\" ({ (N1 . i) where i be Element of N1 : i >= j },R1)) where j be Element of N1;

      set X2 = the set of all ( "/\" ({ (N2 . i) where i be Element of N2 : i >= j },R2)) where j be Element of N2;

      X1 = X2

      proof

        thus X1 c= X2

        proof

          let e be object;

          assume e in X1;

          then

          consider j1 be Element of N1 such that

           A3: e = ( "/\" ({ (N1 . i) where i be Element of N1 : i >= j1 },R1));

          reconsider j2 = j1 as Element of N2 by A2;

          set Y1 = { (N1 . i) where i be Element of N1 : i >= j1 }, Y2 = { (N2 . i) where i be Element of N2 : i >= j2 };

          Y1 = Y2

          proof

            thus Y1 c= Y2

            proof

              let u be object;

              assume u in Y1;

              then

              consider i1 be Element of N1 such that

               A4: u = (N1 . i1) and

               A5: j1 <= i1;

              reconsider i2 = i1 as Element of N2 by A2;

              (N2 . i2) = u by A2, A4;

              hence thesis by A2, A5;

            end;

            let u be object;

            assume u in Y2;

            then

            consider i2 be Element of N2 such that

             A6: u = (N2 . i2) and

             A7: j2 <= i2;

            reconsider i1 = i2 as Element of N1 by A2;

            (N1 . i1) = u by A2, A6;

            hence thesis by A2, A7;

          end;

          then e = ( "/\" (Y2,R2)) by A1, A3, Lm13;

          hence thesis;

        end;

        let e be object;

        assume e in X2;

        then

        consider j1 be Element of N2 such that

         A8: e = ( "/\" ({ (N2 . i) where i be Element of N2 : i >= j1 },R2));

        reconsider j2 = j1 as Element of N1 by A2;

        set Y1 = { (N2 . i) where i be Element of N2 : i >= j1 }, Y2 = { (N1 . i) where i be Element of N1 : i >= j2 };

        Y1 = Y2

        proof

          thus Y1 c= Y2

          proof

            let u be object;

            assume u in Y1;

            then

            consider i1 be Element of N2 such that

             A9: u = (N2 . i1) and

             A10: j1 <= i1;

            reconsider i2 = i1 as Element of N1 by A2;

            (N1 . i2) = u by A2, A9;

            hence thesis by A2, A10;

          end;

          let u be object;

          assume u in Y2;

          then

          consider i2 be Element of N1 such that

           A11: u = (N1 . i2) and

           A12: j2 <= i2;

          reconsider i1 = i2 as Element of N2 by A2;

          (N2 . i1) = u by A2, A11;

          hence thesis by A2, A12;

        end;

        then e = ( "/\" (Y2,R1)) by A1, A8, Lm13;

        hence thesis;

      end;

      hence thesis by A1, Lm12;

    end;

    

     Lm17: for R1,R2 be non empty reflexive RelStr, X be non empty set holds for N1 be net of R1, N2 be net of R2 st N1 = N2 holds for J1 be net_set of the carrier of N1, R1, J2 be net_set of the carrier of N2, R2 st J1 = J2 holds ( Iterated J1) = ( Iterated J2)

    proof

      let R1,R2 be non empty reflexive RelStr, X be non empty set;

      let N1 be net of R1, N2 be net of R2 such that

       A1: N1 = N2;

      let J1 be net_set of the carrier of N1, R1, J2 be net_set of the carrier of N2, R2 such that

       A2: J1 = J2;

      

       A3: the RelStr of ( Iterated J1) = [:N1, ( product J1):] by YELLOW_6:def 13;

      

       A4: the RelStr of ( Iterated J2) = [:N2, ( product J2):] by YELLOW_6:def 13;

      set f = the mapping of ( Iterated J1), g = the mapping of ( Iterated J2);

      

       A5: ( dom f) = the carrier of ( Iterated J2) by A1, A2, A3, A4, FUNCT_2:def 1

      .= ( dom g) by FUNCT_2:def 1;

      for x be object st x in ( dom f) holds (f . x) = (g . x)

      proof

        let x be object;

        assume x in ( dom f);

        then x in the carrier of ( Iterated J1);

        then x in [:the carrier of N1, the carrier of ( product J1):] by A3, YELLOW_3:def 2;

        then

        consider x1 be Element of N1, x2 be Element of ( product J1) such that

         A6: x = [x1, x2] by DOMAIN_1: 1;

        reconsider y1 = x1 as Element of N2 by A1;

        reconsider y2 = x2 as Element of ( product J2) by A1, A2;

        

        thus (f . x) = (the mapping of ( Iterated J1) . (x1,x2)) by A6

        .= (the mapping of (J1 . x1) . (x2 . x1)) by YELLOW_6:def 13

        .= (the mapping of (J2 . y1) . (y2 . y1)) by A2

        .= (the mapping of ( Iterated J2) . (y1,y2)) by YELLOW_6:def 13

        .= (g . x) by A6;

      end;

      then f = g by A5, FUNCT_1: 2;

      hence thesis by A1, A2, A3, A4;

    end;

    

     Lm18: for R1,R2 be non empty reflexive RelStr, X be non empty set st the RelStr of R1 = the RelStr of R2 holds for N1 be net of R1, N2 be net of R2 st N1 = N2 holds for J1 be net_set of the carrier of N1, R1 holds J1 is net_set of the carrier of N2, R2

    proof

      let R1,R2 be non empty reflexive RelStr, X be non empty set such that

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

      let N1 be net of R1, N2 be net of R2 such that

       A2: N1 = N2;

      let J1 be net_set of the carrier of N1, R1;

      reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2;

      for i be set st i in ( rng J2) holds i is net of R2

      proof

        let i be set;

        assume i in ( rng J2);

        then

        reconsider N = i as net of R1 by YELLOW_6:def 12;

        N is NetStr over R2 by A1;

        hence thesis;

      end;

      hence thesis by YELLOW_6:def 12;

    end;

    

     Lm19: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds ( Scott-Convergence R1) c= ( Scott-Convergence R2)

    proof

      let R1,R2 be complete LATTICE such that

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

      

       A2: ( Scott-Convergence R1) c= [:( NetUniv R1), the carrier of R1:] by YELLOW_6:def 18;

      for e be object st e in ( Scott-Convergence R1) holds e in ( Scott-Convergence R2)

      proof

        let e be object;

        assume

         A3: e in ( Scott-Convergence R1);

        then

        consider N1 be Element of ( NetUniv R1), p1 be Element of R1 such that

         A4: e = [N1, p1] by A2, DOMAIN_1: 1;

        

         A5: N1 in ( NetUniv R1);

        

         A6: ex N be strict net of R1 st (N1 = N) & (the carrier of N in ( the_universe_of the carrier of R1)) by YELLOW_6:def 11;

        then

        reconsider N2 = N1 as strict net of R2 by A1, Lm4;

        reconsider N1 as strict net of R1 by A6;

        reconsider p2 = p1 as Element of R2 by A1;

        

         A7: N2 in ( NetUniv R2) by A1, A5, Lm5;

        

         A8: ( lim_inf N1) = ( lim_inf N2) by A1, Lm16;

        p1 is_S-limit_of N1 by A3, A4, Def8;

        then p1 <= ( lim_inf N1);

        then p2 <= ( lim_inf N2) by A1, A8, Lm1;

        then p2 is_S-limit_of N2;

        hence thesis by A4, A7, Def8;

      end;

      hence thesis;

    end;

    

     Lm20: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds ( Scott-Convergence R1) = ( Scott-Convergence R2) by Lm19;

    

     Lm21: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 holds ( sigma R1) = ( sigma R2)

    proof

      let R1,R2 be complete LATTICE;

      assume

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

      set T1 = ( ConvergenceSpace ( Scott-Convergence R1)), T2 = ( ConvergenceSpace ( Scott-Convergence R2));

      

       A2: the topology of T1 = { V where V be Subset of R1 : for p be Element of R1 st p in V holds for N be net of R1 st [N, p] in ( Scott-Convergence R1) holds N is_eventually_in V } by YELLOW_6:def 24;

      

       A3: the topology of T2 = { V where V be Subset of R2 : for p be Element of R2 st p in V holds for N be net of R2 st [N, p] in ( Scott-Convergence R2) holds N is_eventually_in V } by YELLOW_6:def 24;

      the topology of T1 = the topology of T2

      proof

        thus the topology of T1 c= the topology of T2

        proof

          let e be object;

          assume e in the topology of T1;

          then

          consider V1 be Subset of R1 such that

           A4: e = V1 and

           A5: for p be Element of R1 st p in V1 holds for N be net of R1 st [N, p] in ( Scott-Convergence R1) holds N is_eventually_in V1 by A2;

          reconsider V2 = V1 as Subset of R2 by A1;

          for p be Element of R2 st p in V2 holds for N be net of R2 st [N, p] in ( Scott-Convergence R2) holds N is_eventually_in V2

          proof

            let p2 be Element of R2 such that

             A6: p2 in V2;

            reconsider p1 = p2 as Element of R1 by A1;

            let N2 be net of R2;

            reconsider N1 = N2 as net of R1 by A1;

            assume [N2, p2] in ( Scott-Convergence R2);

            then [N1, p1] in ( Scott-Convergence R1) by A1, Lm20;

            hence thesis by A5, A6, Lm6;

          end;

          hence thesis by A3, A4;

        end;

        let e be object;

        assume e in the topology of T2;

        then

        consider V1 be Subset of R2 such that

         A7: e = V1 and

         A8: for p be Element of R2 st p in V1 holds for N be net of R2 st [N, p] in ( Scott-Convergence R2) holds N is_eventually_in V1 by A3;

        reconsider V2 = V1 as Subset of R1 by A1;

        for p be Element of R1 st p in V2 holds for N be net of R1 st [N, p] in ( Scott-Convergence R1) holds N is_eventually_in V2

        proof

          let p2 be Element of R1 such that

           A9: p2 in V2;

          reconsider p1 = p2 as Element of R2 by A1;

          let N2 be net of R1;

          reconsider N1 = N2 as net of R2 by A1;

          assume [N2, p2] in ( Scott-Convergence R1);

          then [N1, p1] in ( Scott-Convergence R2) by A1, Lm20;

          hence thesis by A8, A9, Lm6;

        end;

        hence thesis by A2, A7;

      end;

      hence thesis;

    end;

    

     Lm22: for R1,R2 be LATTICE st the RelStr of R1 = the RelStr of R2 & R1 is complete holds R2 is complete

    proof

      let R1,R2 be LATTICE such that

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

       A2: R1 is complete;

      let X be set;

      consider a1 be Element of R1 such that

       A3: X is_<=_than a1 and

       A4: for b be Element of R1 st X is_<=_than b holds a1 <= b by A2;

      reconsider a2 = a1 as Element of R2 by A1;

      take a2;

      thus X is_<=_than a2 by A1, A3, Lm10;

      let b2 be Element of R2;

      reconsider b1 = b2 as Element of R1 by A1;

      assume X is_<=_than b2;

      then X is_<=_than b1 by A1, Lm10;

      hence a2 <= b2 by A1, A4, Lm1;

    end;

    

     Lm23: for R1,R2 be complete LATTICE st the RelStr of R1 = the RelStr of R2 & R1 is continuous holds R2 is continuous

    proof

      let R1,R2 be complete LATTICE such that

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

      assume

       A2: R1 is continuous;

      thus

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

      thus R2 is up-complete;

      for x,y be Element of R2 st not x <= y holds ex u be Element of R2 st u << x & not u <= y

      proof

        let x2,y2 be Element of R2;

        reconsider x1 = x2, y1 = y2 as Element of R1 by A1;

        assume not x2 <= y2;

        then not x1 <= y1 by A1, Lm1;

        then

        consider u1 be Element of R1 such that

         A4: u1 << x1 and

         A5: not u1 <= y1 by A2, WAYBEL_3: 24;

        reconsider u2 = u1 as Element of R2 by A1;

        take u2;

        thus u2 << x2 by A1, A4, Lm15;

        thus thesis by A1, A5, Lm1;

      end;

      hence thesis by A3, WAYBEL_3: 24;

    end;

    registration

      let R be continuous complete LATTICE;

      cluster ( Scott-Convergence R) -> topological;

      coherence

      proof

        set C = ( Scott-Convergence R);

        thus C is (CONSTANTS) (SUBNETS);

        thus C is (DIVERGENCE)

        proof

          let X be net of R, p be Element of R such that

           A1: X in ( NetUniv R) and

           A2: not [X, p] in C;

          

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

          reconsider p9 = p as Element of R;

          consider N be strict net of R such that

           A4: N = X and the carrier of N in ( the_universe_of the carrier of R) by A1, YELLOW_6:def 11;

           not p is_S-limit_of N by A1, A2, A4, Def8;

          then not p <= ( lim_inf X) by A4;

          then

          consider u be Element of R such that

           A5: u << p9 and

           A6: not u <= ( lim_inf X) by A3, WAYBEL_3: 24;

          set A = { a where a be Element of R : not a >= u };

          X is_often_in A

          proof

            let i be Element of X;

            set B = { (X . j) where j be Element of X : j >= i };

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

            ( "/\" (B,R)) in C;

            then ( "/\" (B,R)) <= ( lim_inf X) by YELLOW_2: 22;

            then not u <= ( "/\" (B,R)) by A6, YELLOW_0:def 2;

            then not u is_<=_than B by YELLOW_0: 33;

            then

            consider b be Element of R such that

             A7: b in B and

             A8: not u <= b;

            consider j be Element of X such that

             A9: b = (X . j) and

             A10: j >= i by A7;

            take j;

            thus i <= j by A10;

            thus thesis by A8, A9;

          end;

          then

          reconsider Y = (X " A) as subnet of X by YELLOW_6: 22;

          take Y;

          reconsider UN = ( the_universe_of the carrier of R) as universal set;

          

           A11: ex N be strict net of R st X = N & the carrier of N in UN by A1, YELLOW_6:def 11;

          (X " A) is SubRelStr of X by YELLOW_6:def 6;

          then the carrier of (X " A) c= the carrier of X by YELLOW_0:def 13;

          then the carrier of Y in UN by A11, CLASSES1:def 1;

          hence Y in ( NetUniv R) by YELLOW_6:def 11;

          let Z be subnet of Y;

          assume

           A12: [Z, p] in C;

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

          then

           A13: Z in ( NetUniv R) by A12, ZFMISC_1: 87;

          then

          consider ZZ be strict net of R such that

           A14: ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 11;

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

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

          D is Subset of R from DOMAIN_1:sch 8;

          then

          reconsider D as Subset of R;

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

          p is_S-limit_of ZZ by A12, A13, A14, Def8;

          then p <= ( lim_inf Z) by A14;

          then

          consider d be Element of R such that

           A15: d in D and

           A16: u <= d by A5;

          consider j be Element of Z such that

           A17: d = ( "/\" ({ (Z . k) where k be Element of Z : k >= j },R)) by A15;

          reconsider j9 = j as Element of Z;

          consider i be Element of Z such that

           A18: i >= j9 and i >= j9 by YELLOW_6:def 3;

          consider f be Function of Z, Y such that

           A19: the mapping of Z = (the mapping of Y * f) and for m be Element of Y holds ex n be Element of Z st for p be Element of Z st n <= p holds m <= (f . p) by YELLOW_6:def 9;

          (Z . i) in { (Z . k) where k be Element of Z : k >= j } by A18;

          then

           A20: d <= (Z . i) by A17, YELLOW_2: 22;

          (Y . (f . i)) = (Z . i) by A19, FUNCT_2: 15;

          then (Z . i) in A by Th35;

          then ex a be Element of R st a = (Z . i) & not a >= u;

          hence contradiction by A16, A20, YELLOW_0:def 2;

        end;

        thus C is (ITERATED_LIMITS)

        proof

          let X be net of R, p be Element of R such that

           A21: [X, p] in C;

          let J be net_set of the carrier of X, R such that

           A22: for i be Element of X holds [(J . i), (X . i)] in C;

          

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

          then

           A24: X in ( NetUniv R) by A21, ZFMISC_1: 87;

          for i be Element of X holds (J . i) in ( NetUniv R)

          proof

            let i be Element of X;

             [(J . i), (X . i)] in C by A22;

            hence thesis by A23, ZFMISC_1: 87;

          end;

          then

           A25: ( Iterated J) in ( NetUniv R) by A24, YELLOW_6: 25;

          reconsider p9 = p as Element of R;

          set q = ( lim_inf ( Iterated J));

          q is_>=_than ( waybelow p9)

          proof

            let u be Element of R;

            assume u in ( waybelow p9);

            then

             A26: u << p9 by WAYBEL_3: 7;

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

            

             A27: the RelStr of T = the RelStr of R;

            

             A28: the carrier of R = the carrier of ( ConvergenceSpace C) by YELLOW_6:def 24;

            then

            reconsider T as TopLattice by A27, Lm3, Lm9;

            reconsider T as complete TopLattice by A27, Lm22;

            reconsider T as continuous complete TopLattice by A27, Lm23;

            the topology of T = ( sigma T) by A27, Lm21;

            then

            reconsider T as continuous complete Scott TopLattice by Th37;

            reconsider XX = X as net of T;

            reconsider JJ = J as net_set of the carrier of XX, T by A27, Lm18;

            reconsider uu = u, qq = q, pp = p9 as Element of T;

            set N = ( Iterated JJ);

            set CC = ( Convergence T);

            CC = ( Convergence ( ConvergenceSpace C)) by A28, Lm8;

            then

             A29: C c= CC by YELLOW_6: 40;

            

             A30: uu << pp by A26, A27, Lm15;

            

             A31: qq = ( lim_inf N) by A27, Lm16, Lm17;

            for i be Element of XX holds [(JJ . i), (XX . i)] in CC

            proof

              let i be Element of XX;

              reconsider ii = i as Element of X;

               [(J . ii), (X . ii)] in C by A22;

              hence thesis by A29;

            end;

            then [N, pp] in CC by A21, A29, YELLOW_6:def 23;

            then

             A32: pp in ( Lim N) by YELLOW_6:def 19;

            pp in ( wayabove uu) by A30;

            then ( wayabove uu) is a_neighborhood of pp by Th36, CONNSP_2: 3;

            then

             A33: N is_eventually_in ( wayabove uu) by A32, YELLOW_6:def 15;

            ( wayabove uu) c= ( uparrow uu) by WAYBEL_3: 11;

            then N is_eventually_in ( uparrow uu) by A33, WAYBEL_0: 8;

            hence u <= q by A27, A31, Lm1, Th18;

          end;

          then ( sup ( waybelow p9)) <= q by YELLOW_0: 32;

          then p <= q by WAYBEL_3:def 5;

          then p is_S-limit_of ( Iterated J);

          hence thesis by A25, Def8;

        end;

      end;

    end

    theorem :: WAYBEL11:38

    for T be continuous complete Scott TopLattice, x be Element of T, N be net of T st N in ( NetUniv T) holds x is_S-limit_of N iff x in ( Lim N)

    proof

      let T be continuous complete Scott TopLattice, x be Element of T, N be net of T such that

       A1: N in ( NetUniv T);

      

       A2: ( Convergence ( ConvergenceSpace ( Scott-Convergence T))) = ( Scott-Convergence T) by YELLOW_6: 44;

      consider M be strict net of T such that

       A3: M = N and the carrier of M in ( the_universe_of the carrier of T) by A1, YELLOW_6:def 11;

       the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence T)) by Th32;

      then

       A4: ( Convergence T) = ( Convergence ( ConvergenceSpace ( Scott-Convergence T))) by Lm8;

      thus x is_S-limit_of N implies x in ( Lim N)

      proof

        assume x is_S-limit_of N;

        then [N, x] in ( Convergence T) by A1, A2, A3, A4, Def8;

        hence thesis by YELLOW_6:def 19;

      end;

      assume x in ( Lim N);

      then [M, x] in ( Scott-Convergence T) by A1, A2, A3, A4, YELLOW_6:def 19;

      hence thesis by A1, A3, Def8;

    end;

    theorem :: WAYBEL11:39

    

     Th39: for L be complete non empty Poset st ( Scott-Convergence L) is (ITERATED_LIMITS) holds L is continuous

    proof

      let L be complete non empty Poset such that

       A1: ( Scott-Convergence L) is (ITERATED_LIMITS);

      set C = ( Scott-Convergence L);

      now

        let I be non empty set such that

         A2: I in ( the_universe_of the carrier of L);

        let K be non-empty ManySortedSet of I such that

         A3: for j be Element of I holds (K . j) in ( the_universe_of the carrier of L);

        let F be DoubleIndexedSet of K, L such that

         A4: for j be Element of I holds ( rng (F . j)) is directed;

        set x = ( Inf ( Sups F));

        

         A5: x >= ( Sup ( Infs ( Frege F))) by WAYBEL_5: 16;

         [:I, I:] c= [:I, I:];

        then

        reconsider r = [:I, I:] as Relation of I;

        ( dom F) = I by PARTFUN1:def 2;

        then

        reconsider f = ( Sups F) as Function of I, the carrier of L;

        set X = NetStr (# I, r, f #);

        

         A6: for i,j be Element of X holds i <= j

        proof

          let i,j be Element of X;

           [i, j] in the InternalRel of X by ZFMISC_1: 87;

          hence thesis by ORDERS_2:def 5;

        end;

        

         A7: X is transitive by A6;

        X is directed

        proof

          let x,y be Element of X;

          take x;

          thus thesis by A6;

        end;

        then

        reconsider X = NetStr (# I, r, f #) as strict net of L by A7;

        deffunc F( Element of I) = ( Net-Str ((K . $1),(F . $1)));

        consider J be ManySortedSet of I such that

         A8: for i be Element of I holds (J . i) = F(i) from PBOOLE:sch 5;

        for i be set st i in the carrier of X holds (J . i) is net of L

        proof

          let i be set;

          assume i in the carrier of X;

          then

          reconsider i9 = i as Element of I;

          reconsider rFi = ( rng (F . i9)) as Subset of L;

          

           A9: rFi is directed by A4;

          (J . i9) = ( Net-Str ((K . i9),(F . i9))) by A8;

          hence thesis by A9, Th20;

        end;

        then

        reconsider J as net_set of the carrier of X, L by YELLOW_6: 24;

        

         A10: for j be set st j in I holds ex R be 1-sorted st R = (J . j) & (K . j) = the carrier of R

        proof

          let i be set;

          assume i in I;

          then

          reconsider i9 = i as Element of I;

          take R = ( Net-Str ((K . i9),(F . i9)));

          thus R = (J . i) by A8;

          thus thesis by Def10;

        end;

        

         A11: ( doms F) = K by YELLOW_7: 45

        .= ( Carrier J) by A10, PRALG_1:def 15;

        

         A12: ( dom ( Frege F)) = ( product ( doms F)) by PARTFUN1:def 2;

        then

         A13: ( dom ( Infs ( Frege F))) = ( product ( doms F)) by FUNCT_2:def 1;

        

         A14: for i be Element of X holds (J . i) in ( NetUniv L)

        proof

          let i be Element of X;

          reconsider i9 = i as Element of I;

          

           A15: (J . i) = ( Net-Str ((K . i9),(F . i9))) by A8;

          then

          reconsider Ji = (J . i) as strict net of L;

          (K . i9) in ( the_universe_of the carrier of L) by A3;

          then the carrier of Ji in ( the_universe_of the carrier of L) by A15, Def10;

          hence thesis by YELLOW_6:def 11;

        end;

        

         A16: for i be Element of X holds [(J . i), (X . i)] in C

        proof

          let i be Element of X;

          reconsider i9 = i as Element of I;

          

           A17: (J . i) = ( Net-Str ((K . i9),(F . i9))) by A8;

          then

          reconsider Ji = (J . i) as monotone reflexive net of L;

          

           A18: (J . i) in ( NetUniv L) by A14;

          i in I;

          then i9 in ( dom F) by PARTFUN1:def 2;

          

          then (X . i) = ( Sup (F . i9)) by WAYBEL_5:def 1

          .= ( Sup the mapping of Ji) by A17, Def10

          .= ( sup Ji) by WAYBEL_2:def 1

          .= ( lim_inf Ji) by Th22;

          then (X . i) is_S-limit_of (J . i);

          hence thesis by A17, A18, Def8;

        end;

        

         A19: X in ( NetUniv L) by A2, YELLOW_6:def 11;

        then

         A20: ( Iterated J) in ( NetUniv L) by A14, YELLOW_6: 25;

        deffunc I( Element of ( Iterated J)) = { (( Iterated J) . p) where p be Element of ( Iterated J) : p >= $1 };

        the carrier of ( Iterated J) = [:the carrier of X, ( product ( Carrier J)):] by YELLOW_6: 26;

        then

        reconsider G = the mapping of ( Iterated J) as Function of [:the carrier of X, ( product ( doms F)):], the carrier of L by A11;

        deffunc I( Element of X, Element of ( product ( doms F))) = { (G . (i,$2)) where i be Element of X : i >= $1 };

        deffunc F( Element of ( product ( doms F))) = ( "/\" (( rng (( Frege F) . $1)),L));

        deffunc F( Element of X, Element of ( product ( doms F))) = ( "/\" ( I($1,$2),L));

        set D = the set of all ( "/\" ( I(j),L)) where j be Element of ( Iterated J);

        set D9 = { F(i,g) where i be Element of X, g be Element of ( product ( doms F)) : P[g] };

        set E9 = { F(g) where g be Element of ( product ( doms F)) : P[g] };

        

         A21: for i be Element of X, g be Element of ( product ( doms F)) holds F(g) = F(i,g)

        proof

          let j be Element of X, g be Element of ( product ( doms F));

          for y be object holds y in I(j,g) iff ex x be object st x in ( dom (( Frege F) . g)) & y = ((( Frege F) . g) . x)

          proof

            let y be object;

            g in ( product ( Carrier J)) by A11;

            then

             A22: g in the carrier of ( product J) by YELLOW_1:def 4;

            hereby

              assume y in I(j,g);

              then

              consider i be Element of X such that

               A23: y = (G . (i,g)) and i >= j;

              reconsider x = i as object;

              take x;

              reconsider i9 = i as Element of I;

              

               A24: i in I;

              then

               A25: i9 in ( dom F) by PARTFUN1:def 2;

              thus x in ( dom (( Frege F) . g)) by A24, PARTFUN1:def 2;

              

              thus ((( Frege F) . g) . x) = ((F . i9) . (g . i)) by A12, A25, WAYBEL_5: 9

              .= (the mapping of ( Net-Str ((K . i9),(F . i9))) . (g . i)) by Def10

              .= (the mapping of (J . i) . (g . i)) by A8

              .= y by A22, A23, YELLOW_6:def 13;

            end;

            given x be object such that

             A26: x in ( dom (( Frege F) . g)) and

             A27: y = ((( Frege F) . g) . x);

            

             A28: x in ( dom F) by A12, A26, WAYBEL_5: 8;

            reconsider i9 = x as Element of I by A26;

            reconsider i = i9 as Element of X;

            

             A29: i >= j by A6;

            y = ((F . x) . (g . x)) by A12, A27, A28, WAYBEL_5: 9

            .= (the mapping of ( Net-Str ((K . i9),(F . i9))) . (g . i)) by Def10

            .= (the mapping of (J . i) . (g . i)) by A8

            .= (G . (i,g)) by A22, YELLOW_6:def 13;

            hence thesis by A29;

          end;

          hence thesis by FUNCT_1:def 3;

        end;

        

         A30: D = D9

        proof

          

           A31: the carrier of ( Iterated J) = [:the carrier of X, ( product ( Carrier J)):] by YELLOW_6: 26;

          

           A32: for p be Element of ( Iterated J), i be Element of X, g be Element of ( product ( doms F)) st p = [i, g] holds ( "/\" ( I(p),L)) = ( "/\" ( I(i,g),L))

          proof

            let p be Element of ( Iterated J), i be Element of X, g be Element of ( product ( doms F)) such that

             A33: p = [i, g];

            

             A34: the RelStr of ( Iterated J) = the RelStr of [:X, ( product J):] by YELLOW_6:def 13;

            reconsider g9 = g as Element of ( product J) by A11, YELLOW_1:def 4;

            g9 in the carrier of ( product J);

            then

             A35: g9 in ( product ( Carrier J)) by YELLOW_1:def 4;

            reconsider i9 = i as Element of X;

            for i be object st i in the carrier of X holds ex R be RelStr, xi,yi be Element of R st R = (J . i) & xi = (g9 . i) & yi = (g9 . i) & xi <= yi

            proof

              let i be object;

              assume i in the carrier of X;

              then

              reconsider ii = i as Element of X;

              reconsider i9 = ii as Element of I;

              

               A36: (J . i) = ( Net-Str ((K . i9),(F . i9))) by A8;

              set R = ( Net-Str ((K . i9),(F . i9)));

              (g9 . ii) in the carrier of R by A36;

              then

              reconsider x = (g9 . i) as Element of R;

              take R, x, x;

              x <= x;

              hence thesis by A8;

            end;

            then

             A37: g9 <= g9 by A35, YELLOW_1:def 4;

             I(i,g) c= I(p)

            proof

              let u be object;

              assume u in I(i,g);

              then

              consider j be Element of X such that

               A38: u = (the mapping of ( Iterated J) . (j,g)) and

               A39: j >= i;

              reconsider j9 = j as Element of X;

              reconsider q = [j, g] as Element of ( Iterated J) by A11, YELLOW_6: 26;

               [j9, g9] >= [i9, g9] by A37, A39, YELLOW_3: 11;

              then

               A40: q >= p by A33, A34, Lm1;

              u = (( Iterated J) . q) by A38;

              hence thesis by A40;

            end;

            then

             A41: ( "/\" ( I(p),L)) <= ( "/\" ( I(i,g),L)) by WAYBEL_7: 1;

            defpred P[ Element of X] means $1 >= i;

            deffunc F( Element of X) = (G . ($1,g));

            { F(k) where k be Element of X : P[k] } is Subset of L from DOMAIN_1:sch 8;

            then

            reconsider A = I(i,g) as Subset of L;

            defpred P[ Element of ( Iterated J)] means $1 >= p;

            deffunc F( Element of ( Iterated J)) = (( Iterated J) . $1);

            { F(z) where z be Element of ( Iterated J) : P[z] } is Subset of L from DOMAIN_1:sch 8;

            then

            reconsider B = I(p) as Subset of L;

            B is_coarser_than A

            proof

              let b be Element of L;

              assume b in B;

              then

              consider q be Element of ( Iterated J) such that

               A42: b = (( Iterated J) . q) and

               A43: p <= q;

              consider k be Element of X, f be Element of ( product ( Carrier J)) such that

               A44: q = [k, f] by A31, DOMAIN_1: 1;

              reconsider k9 = k as Element of X;

              set a = (the mapping of ( Iterated J) . (k,g));

              a = (G . (k,g));

              then

              reconsider a as Element of L;

              take a;

              reconsider f9 = f as Element of ( product J) by YELLOW_1:def 4;

              

               A45: [k9, f9] >= [i9, g9] by A33, A34, A43, A44, Lm1;

              then i <= k by YELLOW_3: 11;

              hence a in A;

              reconsider k9 = k as Element of I;

              set N = ( Net-Str ((K . k9),(F . k9)));

              

               A46: (J . k) = N by A8;

              reconsider g9k = (g9 . k), f9k = (f9 . k) as Element of N by A8;

              

               A47: b = (N . f9k) by A42, A44, A46, YELLOW_6: 27;

              reconsider kg = [k, g] as Element of ( Iterated J) by A11, YELLOW_6: 26;

              

               A48: a = (( Iterated J) . kg)

              .= (N . g9k) by A46, YELLOW_6: 27;

              g9 <= f9 by A45, YELLOW_3: 11;

              then (g9 . k) <= (f9 . k) by WAYBEL_3: 28;

              hence a <= b by A46, A47, A48, Def10;

            end;

            then ( "/\" ( I(i,g),L)) <= ( "/\" ( I(p),L)) by Th1;

            hence thesis by A41, YELLOW_0:def 3;

          end;

          thus D c= D9

          proof

            let e be object;

            assume e in D;

            then

            consider p be Element of ( Iterated J) such that

             A49: e = ( "/\" ( I(p),L));

            consider j be Element of X, g be Element of ( product ( doms F)) such that

             A50: p = [j, g] by A11, A31, DOMAIN_1: 1;

            e = ( "/\" ( I(j,g),L)) by A32, A49, A50;

            hence thesis;

          end;

          let e be object;

          assume e in D9;

          then

          consider i be Element of X, g be Element of ( product ( doms F)) such that

           A51: e = ( "/\" ( I(i,g),L));

          reconsider j = [i, g] as Element of ( Iterated J) by A11, YELLOW_6: 26;

          e = ( "/\" ( I(j),L)) by A32, A51;

          hence thesis;

        end;

        

         A52: E9 = D9 from Irrel( A21);

        for y be object holds y in E9 iff ex x be object st x in ( dom ( Infs ( Frege F))) & y = (( Infs ( Frege F)) . x)

        proof

          let y be object;

          thus y in E9 implies ex x be object st x in ( dom ( Infs ( Frege F))) & y = (( Infs ( Frege F)) . x)

          proof

            assume y in E9;

            then

            consider g be Element of ( product ( doms F)) such that

             A53: y = ( "/\" (( rng (( Frege F) . g)),L));

            take g;

            thus

             A54: g in ( dom ( Infs ( Frege F))) by A13;

            

            thus y = ( //\ ((( Frege F) . g),L)) by A53, YELLOW_2:def 6

            .= (( Infs ( Frege F)) . g) by A54, WAYBEL_5:def 2;

          end;

          given x be object such that

           A55: x in ( dom ( Infs ( Frege F))) and

           A56: y = (( Infs ( Frege F)) . x);

          reconsider x as Element of ( product ( doms F)) by A55, PARTFUN1:def 2;

          y = ( //\ ((( Frege F) . x),L)) by A55, A56, WAYBEL_5:def 2

          .= ( "/\" (( rng (( Frege F) . x)),L)) by YELLOW_2:def 6;

          hence thesis;

        end;

        then ( rng ( Infs ( Frege F))) = E9 by FUNCT_1:def 3;

        then

         A57: ( Sup ( Infs ( Frege F))) = ( lim_inf ( Iterated J)) by A30, A52, YELLOW_2:def 5;

        reconsider x9 = x as Element of L;

        set X1 = the set of all x where j9 be Element of X;

        set X2 = the set of all ( "/\" ({ (X . i) where i be Element of X : i >= j },L)) where j be Element of X;

        

         A58: X2 = X1

        proof

          

           A59: for j be Element of X holds x = ( "/\" ({ (X . i) where i be Element of X : i >= j },L))

          proof

            let j be Element of X;

            set X3 = { (X . i) where i be Element of X : i >= j };

            for e be object holds e in X3 iff ex u be object st u in ( dom ( Sups F)) & e = (( Sups F) . u)

            proof

              let e be object;

              hereby

                assume e in X3;

                then

                consider i be Element of X such that

                 A60: e = (X . i) and i >= j;

                reconsider u = i as object;

                take u;

                u in I;

                hence u in ( dom ( Sups F)) by FUNCT_2:def 1;

                thus e = (( Sups F) . u) by A60;

              end;

              given u be object such that

               A61: u in ( dom ( Sups F)) and

               A62: e = (( Sups F) . u);

              reconsider i = u as Element of X by A61, FUNCT_2:def 1;

              

               A63: i >= j by A6;

              e = (X . i) by A62;

              hence thesis by A63;

            end;

            then ( rng ( Sups F)) = X3 by FUNCT_1:def 3;

            hence thesis by YELLOW_2:def 6;

          end;

          thus X2 c= X1

          proof

            let u be object;

            assume u in X2;

            then ex j be Element of X st (u = ( "/\" ({ (X . i) where i be Element of X : i >= j },L)));

            then u = x by A59;

            hence thesis;

          end;

          let u be object;

          set j = the Element of X;

          assume u in X1;

          then ex j be Element of X st u = x;

          then u = ( "/\" ({ (X . i) where i be Element of X : i >= j },L)) by A59;

          hence thesis;

        end;

        now

          let u be object;

          u in X1 iff ex j9 be Element of X st u = x;

          then u in X1 iff u = x;

          hence u in X1 iff u in {x} by TARSKI:def 1;

        end;

        

        then ( "\/" (X2,L)) = ( sup {x9}) by A58, TARSKI: 2

        .= x by YELLOW_0: 39;

        then x <= ( lim_inf X);

        then x is_S-limit_of X;

        then [X, x] in C by A19, Def8;

        then [( Iterated J), x] in C by A1, A16;

        then x is_S-limit_of ( Iterated J) by A20, Def8;

        then x <= ( Sup ( Infs ( Frege F))) by A57;

        hence x = ( Sup ( Infs ( Frege F))) by A5, ORDERS_2: 2;

      end;

      hence thesis by WAYBEL_5: 18;

    end;

    theorem :: WAYBEL11:40

    for T be complete Scott TopLattice holds T is continuous iff ( Convergence T) = ( Scott-Convergence T)

    proof

      let T be complete Scott TopLattice;

      hereby

        assume T is continuous;

        then

        reconsider L = T as continuous complete Scott TopLattice;

         the TopStruct of T = ( ConvergenceSpace ( Scott-Convergence T)) by Th32;

        

        hence ( Convergence T) = ( Convergence ( ConvergenceSpace ( Scott-Convergence L))) by Lm8

        .= ( Scott-Convergence T) by YELLOW_6: 44;

      end;

      thus thesis by Th39;

    end;

    theorem :: WAYBEL11:41

    

     Th41: for T be complete Scott TopLattice, S be upper Subset of T st S is Open holds S is open

    proof

      let T be complete Scott TopLattice, S be upper Subset of T such that

       A1: for x be Element of T st x in S holds ex y be Element of T st y in S & y << x;

      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

         A2: y in S and

         A3: y << ( sup D) by A1;

        consider d be Element of T such that

         A4: d in D and

         A5: y <= d by A3;

        d in S by A2, A5, WAYBEL_0:def 20;

        hence thesis by A4, XBOOLE_0: 3;

      end;

      hence thesis by Def4;

    end;

    theorem :: WAYBEL11:42

    

     Th42: for L be non empty RelStr, S be upper Subset of L, x be Element of L st x in S holds ( uparrow x) c= S

    proof

      let L be non empty RelStr, S be upper Subset of L, x be Element of L;

      assume

       A1: x in S;

      let e be object;

      assume

       A2: e in ( uparrow x);

      then

      reconsider y = e as Element of L;

      x <= y by A2, WAYBEL_0: 18;

      hence thesis by A1, WAYBEL_0:def 20;

    end;

    theorem :: WAYBEL11:43

    

     Th43: for L be complete continuous Scott TopLattice, p be Element of L, S be Subset of L st S is open & p in S holds ex q be Element of L st q << p & q in S

    proof

      let L be complete continuous Scott TopLattice, p be Element of L;

      let S be Subset of L such that

       A1: S is open and

       A2: p in S;

      

       A3: S is inaccessible by A1, Def4;

      ( sup ( waybelow p)) = p by WAYBEL_3:def 5;

      then ( waybelow p) meets S by A2, A3;

      then (( waybelow p) /\ S) <> {} ;

      then

      consider u be Element of L such that

       A4: u in (( waybelow p) /\ S) by SUBSET_1: 4;

      reconsider u as Element of L;

      take u;

      u in ( waybelow p) by A4, XBOOLE_0:def 4;

      hence u << p by WAYBEL_3: 7;

      thus thesis by A4, XBOOLE_0:def 4;

    end;

    theorem :: WAYBEL11:44

    

     Th44: for L be complete continuous Scott TopLattice, p be Element of L holds { ( wayabove q) where q be Element of L : q << p } is Basis of p

    proof

      let L be complete continuous Scott TopLattice, p be Element of L;

      set X = { ( wayabove q) where q be Element of L : q << p };

      X c= ( bool the carrier of L)

      proof

        let e be object;

        assume e in X;

        then ex q be Element of L st e = ( wayabove q) & q << p;

        hence thesis;

      end;

      then

      reconsider X as Subset-Family of L;

      X is Basis of p

      proof

        

         A1: X is open

        proof

          let e be Subset of L;

          assume e in X;

          then

          consider q be Element of L such that

           A2: e = ( wayabove q) and q << p;

          ( wayabove q) is open by Th36;

          hence thesis by A2;

        end;

        X is p -quasi_basis

        proof

          for Y be set st Y in X holds p in Y

          proof

            let e be set;

            assume e in X;

            then ex q be Element of L st e = ( wayabove q) & q << p;

            hence thesis;

          end;

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

          let S be Subset of L such that

           A3: S is open and

           A4: p in S;

          consider u be Element of L such that

           A5: u << p and

           A6: u in S by A3, A4, Th43;

          take V = ( wayabove u);

          thus V in X by A5;

          

           A7: S is upper by A3, Def4;

          

           A8: ( wayabove u) c= ( uparrow u) by WAYBEL_3: 11;

          ( uparrow u) c= S by A6, A7, Th42;

          hence thesis by A8;

        end;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: WAYBEL11:45

    

     Th45: for T be complete continuous Scott TopLattice holds the set of all ( wayabove x) where x be Element of T is Basis of T

    proof

      let T be complete continuous Scott TopLattice;

      set B = the set of all ( wayabove x) where x be Element of T;

      

       A1: B c= the topology of T

      proof

        let e be object;

        assume e in B;

        then

        consider x be Element of T such that

         A2: e = ( wayabove x);

        ( wayabove x) is open by Th36;

        hence thesis by A2;

      end;

      then

      reconsider P = B as Subset-Family of T by XBOOLE_1: 1;

      for x be Point of T holds ex B be Basis of x st B c= P

      proof

        let x be Point of T;

        reconsider p = x as Element of T;

        reconsider A = { ( wayabove q) where q be Element of T : q << p } as Basis of x by Th44;

        take A;

        let u be object;

        assume u in A;

        then ex q be Element of T st u = ( wayabove q) & q << p;

        hence thesis;

      end;

      hence thesis by A1, YELLOW_8: 14;

    end;

    theorem :: WAYBEL11:46

    for T be complete continuous Scott TopLattice, S be upper Subset of T holds S is open iff S is Open

    proof

      let T be complete continuous Scott TopLattice, S be upper Subset of T;

      thus S is open implies S is Open

      proof

        assume

         A1: S is open;

        let x be Element of T;

        assume x in S;

        then ex y be Element of T st y << x & y in S by A1, Th43;

        hence thesis;

      end;

      thus thesis by Th41;

    end;

    theorem :: WAYBEL11:47

    for T be complete continuous Scott TopLattice, p be Element of T holds ( Int ( uparrow p)) = ( wayabove p)

    proof

      let T be complete continuous Scott TopLattice, p be Element of T;

      thus ( Int ( uparrow p)) c= ( wayabove p)

      proof

        let y be object;

        assume

         A1: y in ( Int ( uparrow p));

        then

        reconsider q = y as Element of T;

        reconsider S = ( Int ( uparrow p)) as Subset of T;

        consider u be Element of T such that

         A2: u << q and

         A3: u in S by A1, Th43;

        S c= ( uparrow p) by TOPS_1: 16;

        then p <= u by A3, WAYBEL_0: 18;

        then p << q by A2, WAYBEL_3: 2;

        hence thesis;

      end;

      ( wayabove p) c= ( uparrow p) by WAYBEL_3: 11;

      hence thesis by Th36, TOPS_1: 24;

    end;

    theorem :: WAYBEL11:48

    for T be complete continuous Scott TopLattice, S be Subset of T holds ( Int S) = ( union { ( wayabove x) where x be Element of T : ( wayabove x) c= S })

    proof

      let T be complete continuous Scott TopLattice, S be Subset of T;

      set B = the set of all ( wayabove x) where x be Element of T;

      set I = { G where G be Subset of T : G in B & G c= S }, P = { ( wayabove x) where x be Element of T : ( wayabove x) c= S };

      

       A1: I = P

      proof

        thus I c= P

        proof

          let e be object;

          assume e in I;

          then

          consider G be Subset of T such that

           A2: e = G and

           A3: G in B and

           A4: G c= S;

          ex x be Element of T st G = ( wayabove x) by A3;

          hence thesis by A2, A4;

        end;

        let e be object;

        assume e in P;

        then

        consider x be Element of T such that

         A5: e = ( wayabove x) and

         A6: ( wayabove x) c= S;

        ( wayabove x) in B;

        hence thesis by A5, A6;

      end;

      B is Basis of T by Th45;

      hence thesis by A1, YELLOW_8: 11;

    end;