The Mizar article:

Scott Topology

by
Andrzej Trybulec

Received January 29, 1997

Copyright (c) 1997 Association of Mizar Users

MML identifier: WAYBEL11
[ MML identifier index ]


environ

 vocabulary ORDERS_1, BHSP_3, WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, QUANTAL1,
      BOOLE, RELAT_2, FINSET_1, ORDINAL2, YELLOW_0, REALSET1, RELAT_1,
      SUBSET_1, WAYBEL_9, PRE_TOPC, NATTRA_1, T_0TOPSP, CONNSP_2, TOPS_1,
      TARSKI, FUNCT_1, YELLOW_6, SEQM_3, CLASSES1, ZF_LANG, YELLOW_2, PROB_1,
      WAYBEL_3, CARD_3, PBOOLE, CLOSURE1, ZF_REFLE, WAYBEL_5, FUNCT_6,
      RLVECT_2, WAYBEL_6, CANTOR_1, WAYBEL11, RLVECT_3;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FINSET_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, STRUCT_0, REALSET1,
      GROUP_1, WAYBEL_6, PRE_TOPC, TOPS_1, CANTOR_1, CONNSP_2, T_0TOPSP,
      TDLAT_3, PBOOLE, CLASSES1, CLASSES2, CARD_3, PRALG_1, ORDERS_1, LATTICE3,
      YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_3, YELLOW_4,
      WAYBEL_2, WAYBEL_3, WAYBEL_5, YELLOW_6, WAYBEL_9, YELLOW_8;
 constructors T_0TOPSP, TOPS_1, TDLAT_3, GROUP_1, WAYBEL_3, WAYBEL_5, YELLOW_4,
      CLASSES1, ORDERS_3, CANTOR_1, WAYBEL_9, YELLOW_8, WAYBEL_1, WAYBEL_6,
      PRALG_2, CLASSES2, CONNSP_2, MEMBERED, PARTFUN1;
 clusters YELLOW_0, STRUCT_0, WAYBEL_0, TDLAT_3, FINSET_1, WAYBEL_3, YELLOW_6,
      PBOOLE, RELSET_1, WAYBEL_5, PRALG_1, PRVECT_1, YELLOW_1, WAYBEL_9,
      LATTICE3, MSUALG_1, CLASSES2, SUBSET_1, FRAENKEL, MEMBERED, ZFMISC_1,
      FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;
 definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, GROUP_1,
      YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, YELLOW_8,
      WAYBEL_6;
 theorems TSP_1, WAYBEL_0, PRE_TOPC, YELLOW_0, TARSKI, SUBSET_1, TOPS_1,
      YELLOW_2, SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1,
      ORDERS_1, GROUP_1, LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7,
      YELLOW_1, YELLOW_3, PBOOLE, BINOP_1, WAYBEL_3, FUNCT_1, FUNCT_2,
      YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1, YELLOW_4, WAYBEL_1, RELAT_1,
      WAYBEL_4, CANTOR_1, YELLOW_8, XBOOLE_0, XBOOLE_1;
 schemes DOMAIN_1, RELSET_1, COMPLSP1, FRAENKEL, PRALG_2, XBOOLE_0;

begin :: Preliminaries

Lm1:
 for R,S being RelStr, p,q being Element of R,
   p',q' being Element of S
    st p = p' & q = q' & the RelStr of R = the RelStr of S
   holds p <= q implies p' <= q'
proof
 let R,S be RelStr, p,q be Element of R,
     p',q' be Element of S such that
A1: p = p' & q = q' & the RelStr of R = the RelStr of S;
 assume p <= q;
  then [p',q'] in the InternalRel of S by A1,ORDERS_1:def 9;
 hence p' <= q' by ORDERS_1:def 9;
end;

scheme Irrel{D,I() -> non empty set, P[set], F(set)->set, F(set,set)-> set}:
 { F(u) where u is Element of D(): P[u]}
  = { F(i,v) where i is Element of I(), v is Element of D(): P[v]}
provided
A1: for i being Element of I(), u being Element of D()
    holds F(u) = F(i,u)
proof
 set A = { F(u) where u is Element of D(): P[u]},
     B = { F(i,v) where i is Element of I(), v is Element of D(): P[v]};
 thus A c= B
  proof let e be set;
    consider i being Element of I();
   assume e in A;
    then consider u being Element of D() such that
A2:   e = F(u) & P[u];
      e = F(i,u) by A1,A2;
   hence e in B by A2;
  end;
 let e be set;
 assume e in B;
  then consider i being Element of I(), u being Element of D() such that
A3: e = F(i,u) & P[u];
    e = F(u) by A1,A3;
 hence e in A by A3;
end;

theorem Th1:
 for L being complete LATTICE,
     X,Y being 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 being Element of L such that
A2:   x in X and
A3:   x <= y by A1,YELLOW_4:def 2;
       "/\"(X,L) <= x by A2,YELLOW_2:24;
    hence "/\"(X,L) <= y by A3,YELLOW_0:def 2;
   end;
 hence "/\"(X,L) <= "/\"(Y,L) by YELLOW_0:33;
end;

theorem Th2:
 for L being complete LATTICE,
     X,Y being 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 being Element of L such that
A2:   y in Y and
A3:   x <= y by A1,YELLOW_4:def 1;
       "\/"(Y,L) >= y by A2,YELLOW_2:24;
    hence "\/"(Y,L) >= x by A3,YELLOW_0:def 2;
   end;
 hence "\/"(X,L) <= "\/"(Y,L) by YELLOW_0:32;
end;

theorem
   for T being RelStr, A being upper Subset of T, B being 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;
     x in B & y in B by A1,A2,XBOOLE_0:def 3;
   then consider z being Element of T such that
A3: z in B and
A4: x <= z and
A5: y <= z by WAYBEL_0:def 1;
  take z;
    x in A by A1,XBOOLE_0:def 3;
  then z in A by A4,WAYBEL_0:def 20;
 hence z in A /\ B by A3,XBOOLE_0:def 3;
 thus x <= z & y <= z by A4,A5;
end;

definition let T be reflexive non empty RelStr;
 cluster non empty directed finite Subset of T;
 existence
  proof consider x being Element of T;
   take {x};
   thus thesis by WAYBEL_0:5;
  end;
end;

theorem Th4: :: uogolnione WAYBEL_3:16
 for T being with_suprema Poset,
     D being 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 being Element of T such that
A1: x in D and
A2: x is_>=_than E by WAYBEL_0:1;
A3: for b being Element of T st D is_<=_than
 b holds b >= x by A1,LATTICE3:def 9;
     for c being Element of T st D is_<=_than c &
     for b being 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 being Element of T st D is_<=_than b holds b >= c;
       x >= c & c >= x by A1,A2,A4,A5,LATTICE3:def 9;
    hence c = x by ORDERS_1:25;
   end;
  then ex_sup_of D,T by A2,A3,YELLOW_0:def 7;
 hence sup D in D by A1,A2,A3,YELLOW_0:def 9;
end;

definition
 cluster trivial reflexive transitive non empty antisymmetric
  with_suprema with_infima finite strict RelStr;
 existence
  proof
      0 in {0} by TARSKI:def 1;
    then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:8;
   reconsider T = RelStr(#{0},r#) as non empty RelStr;
   take T;
   thus T is trivial;
   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 x <= x by ORDERS_1:def 9;
    end;
    then reconsider T' = T as trivial non empty reflexive RelStr;
      T' is transitive;
   hence T is transitive;
   thus T is non empty;
      T' is antisymmetric;
   hence T is antisymmetric;
      T' is with_suprema;
   hence T is with_suprema;
      T' is with_infima;
   hence T is with_infima;
   thus T is finite by GROUP_1:def 13;
   thus thesis;
  end;
end;

definition
 cluster finite non empty strict 1-sorted;
 existence
  proof
   take S = 1-sorted(#{{}}#);
   thus the carrier of S is finite non empty;
   thus thesis;
  end;
end;

definition let T be finite 1-sorted;
 cluster -> finite Subset of T;
 coherence
  proof let S be Subset of T;
    reconsider C = the carrier of T as finite set by GROUP_1:def 13;
      S is Subset of C;
   hence S is finite;
  end;
end;

definition let R be RelStr;
 cluster {}R -> lower upper;
 coherence
  proof
   thus for x,y being Element of R st x in {}R & y <= x holds y in {}R;
   thus for x,y being Element of R st x in {}R & x <= y holds y in {}R;
  end;
end;

definition let R be trivial non empty RelStr;
 cluster -> upper Subset of R;
 coherence
  proof let S be Subset of R;
    consider x being Element of R such that
A1:   the carrier of R = {x} by TEX_1:def 1;
      S = {} or S = the carrier of R by A1,ZFMISC_1:39;
    then S = {}R or S = [#]R by PRE_TOPC:12;
   hence S is upper;
  end;
end;

theorem Th5:
 for T being non empty RelStr, x being Element of T,
     A being 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 being set 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 Th6:
 for T being non empty RelStr, x being Element of T,
     A being 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 YELLOW_6:10;
  then A` misses downarrow x by Th5;
  then A` c= (downarrow x)` by PRE_TOPC:21;
 hence downarrow x c= A by PRE_TOPC:19;
end;

begin :: Scott Topology

definition let T be non empty reflexive RelStr, S be Subset of T;
 attr S is inaccessible_by_directed_joins means
:Def1:
  for D being non empty directed Subset of T st sup D in S holds D meets S;
 synonym S is inaccessible;
 attr S is closed_under_directed_sups means
:Def2: for D being non empty directed Subset of T st D c= S holds sup D in S;
 synonym S is directly_closed;
 attr S is property(S) means
:Def3: for D being non empty directed Subset of T st sup D in S
  ex y being Element of T st y in D &
   for x being Element of T st x in D & x >= y holds x in S;
 synonym S has_the_property_(S);
end;

definition
 let T be non empty reflexive RelStr;
  cluster {}T -> property(S) directly_closed;
 coherence
  proof
      for D being non empty directed Subset of T st sup D in {}T
     ex y being Element of T st y in D &
      for x being Element of T st x in D & x >= y holds x in {}T;
   hence {}T is property(S) by Def3;
   thus for D being non empty directed Subset of T st D c= {}T holds sup D in
 {}
T
             by XBOOLE_1:3;
  end;
end;

definition
 let T be non empty reflexive RelStr;
  cluster property(S) directly_closed Subset of T;
 existence proof take {}T; thus thesis; end;
end;

definition
 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 YELLOW_6:10;
    then consider y being Element of T such that
A2:  y in D and
A3:  for x being 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 3;
    then D meets S by XBOOLE_0:def 7;
   hence contradiction by A1,PRE_TOPC:21;
  end;
end;

definition let T be reflexive non empty TopRelStr;
 attr T is Scott means
:Def4: for S being Subset of T holds
   S is open iff S is inaccessible upper;
end;

definition
 let T be reflexive transitive antisymmetric non empty with_suprema
   finite RelStr;
 cluster -> inaccessible 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 D meets S by A1,XBOOLE_0:3;
  end;
end;

definition
 let T be reflexive transitive antisymmetric non empty with_suprema
    finite TopRelStr;
 redefine attr T is Scott means
           for S being Subset of T holds S is open iff S is upper;
 compatibility
  proof
   thus T is Scott implies
    for S being Subset of T holds S is open iff S is upper by Def4;
   assume
A1:  for S being Subset of T holds S is open iff S is upper;
   let S be Subset of T;
   thus S is open iff S is inaccessible upper by A1;
  end;
end;

definition
 cluster trivial complete strict non empty Scott TopLattice;
 existence
  proof consider T being
      trivial reflexive non empty discrete strict finite TopRelStr;
   take T;
   thus T is trivial complete strict non empty;
   let S be Subset of T;
   thus S is open iff S is upper by TDLAT_3:17;
  end;
end;

definition let T be non empty reflexive RelStr;
 cluster [#]T -> directly_closed inaccessible;
 coherence
  proof
   thus [#]T is directly_closed
    proof let D be non empty directed Subset of T such that D c= [#]T;
     thus sup D in [#]T by PRE_TOPC:13;
    end;
   let D be non empty directed Subset of T such that sup D in [#]T;
    consider p being Element of T such that
A1:   p in D by SUBSET_1:10;
      p in [#]T by PRE_TOPC:13;
   hence D meets [#]T by A1,XBOOLE_0:3;
  end;
end;

definition let T be non empty reflexive RelStr;
 cluster directly_closed lower inaccessible upper Subset of T;
 existence
  proof take [#]T;
   thus [#]T is directly_closed lower inaccessible upper;
  end;
end;

definition
 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 PRE_TOPC:21;
    then not sup D in S by Def1;
   hence sup D in S` by YELLOW_6:10;
  end;
end;

definition
 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 YELLOW_6:10;
    then not D c= S by Def2;
    then not D c= S``;
    hence D meets S` by PRE_TOPC:21;
  end;
end;

theorem Th7:  :: p. 100, Remark 1.4 (i)
 for T being up-complete Scott (non empty reflexive transitive TopRelStr),
     S being 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 by TOPS_1:29;
   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 by TOPS_1:29;
end;

theorem Th8:
 for T being up-complete (non empty reflexive transitive antisymmetric
     TopRelStr),
     x being 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 being Element of T st a is_>=_than D &
            for b being 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
           proof let b be Element of T;
            assume b in D;
            hence b <= x by A1,WAYBEL_0:17;
           end;
          then sup D <= x by A2,YELLOW_0:30;
         hence sup D in downarrow x by WAYBEL_0:17;
        end;
    hence thesis;
   end;

theorem Th9:  :: p. 100, Remark 1.4 (ii)
 for T being complete Scott TopLattice, x being 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:37;
     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:37;
    hence downarrow x c= C by A4,Th6;
   end;
 hence Cl {x} = downarrow x by A1,A2,YELLOW_8:17;
end;

theorem  :: p. 100, Remark 1.4 (iii)
   for T being 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 x' = x, y' = y as Element of T;
A1:  Cl {x'} = downarrow x' & Cl {y'} = downarrow y' by Th9;
    assume x <> y;
    hence Cl {x} <> Cl {y} by A1,WAYBEL_0:19;
  end;
 hence thesis by TSP_1:def 5;
end;

theorem Th11:
 for T being Scott up-complete (non empty reflexive transitive antisymmetric
     TopRelStr),
     x being Element of T holds
  downarrow x is closed
   proof let T be Scott up-complete
              (non empty reflexive transitive antisymmetric TopRelStr),
             x be Element of T;
      downarrow x is directly_closed lower by Th8;
    hence downarrow x is closed by Th7;
   end;

theorem Th12:
 for T being up-complete Scott TopLattice, x being 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 (downarrow x)` is open by TOPS_1:29;
end;

theorem Th13:
 for T being up-complete Scott TopLattice, x being Element of T,
     A being 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:55;
    A misses downarrow x by A1,Th5;
  then A c= (downarrow x)` by PRE_TOPC:21;
 hence (downarrow x)` is a_neighborhood of A by A2,CONNSP_2:def 2;
end;

theorem  :: p. 100, Remark 1.4 (iv)
   for T being complete Scott TopLattice,
     S being upper Subset of T
  ex F being Subset-Family of T st S = meet F &
   for X being 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 is Subset of T: P[X]};
    F is Subset of bool the carrier of T from SubsetD;
  then F is Subset-Family of T by SETFAM_1:def 7;
  then reconsider F as Subset-Family of T;
 take F;
 thus S = meet F
  proof
     [#]T is a_neighborhood of S by YELLOW_6:7;
   then A1: [#]T in F;
      now let Z1 be set;
     assume Z1 in F;
      then ex X being Subset of T
         st Z1 = X & X is a_neighborhood of S;
     hence S c= Z1 by YELLOW_6:8;
    end;
   hence S c= meet F by A1,SETFAM_1:6;
   let x be set 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:4;
       p <= p;
     then p in downarrow p by WAYBEL_0:17;
   hence contradiction by A2,A4,YELLOW_6:10;
  end;
 let X be Subset of T;
 assume X in F;
  then ex Y being Subset of T st X = Y & Y is a_neighborhood of
S;
 hence X is a_neighborhood of S;
end;

theorem  :: p. 100, Remark 1.4 (v)
   for T being Scott TopLattice,
     S being 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 has_the_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,Def1;
     then consider y being set 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,WAYBEL_0:def 20;
   end;
 end;
 assume that
A6: S is upper and
A7: S has_the_property_(S);
    S is inaccessible
   proof let D be non empty directed Subset of T;
    assume sup D in S;
     then consider y being Element of T such that
A8:    y in D and
A9:    for x being Element of T st x in D & x >= y holds x in S by A7,Def3;
       y >= y by YELLOW_0:def 1;
     then y in S by A8,A9;
    hence D meets S by A8,XBOOLE_0:3;
   end;
 hence S is open by A6,Def4;
end;

definition let T be complete TopLattice;
                  :: p. 100, Remark 1.4 (vi)
 cluster lower -> property(S) 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 being Element of T such that
A3:  y in D by SUBSET_1:10;
   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:24;
   hence x in S by A1,A2,WAYBEL_0:def 19;
  end;
end;

Lm2:
 for T being non empty reflexive TopRelStr
  holds [#]T has_the_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 being Element of T such that
A1:  y in D by SUBSET_1:10;
  take y;
  thus y in D by A1;
  let x be Element of T such that x in D & x >= y;
  thus x in [#]T by PRE_TOPC:13;
 end;

theorem  :: p. 100, Remark 1.4 (vii)
   for T being non empty transitive reflexive TopRelStr st
  the topology of T = { S where S is Subset of T: S has_the_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 is Subset of T: S has_the_property_(S)};
    [#]T has_the_property_(S) by Lm2;
  then [#]T in the topology of T by A1;
 hence the carrier of T in the topology of T by PRE_TOPC:12;
 hereby let a be Subset-Family of T such that
A2: a c= the topology of T;
      union a has_the_property_(S)
     proof let D be non empty directed Subset of T;
      assume sup D in union a;
       then consider x being 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 being Subset of T such that
A5:     x = X and
A6:     X has_the_property_(S) by A1;
       consider y being Element of T such that
A7:     y in D and
A8:     for x being Element of T st x in D & x >=
 y holds x in X by A3,A5,A6,Def3;
      take y;
      thus y in D by A7;
      let u be Element of T;
      assume u in D & u >= y;
       then u in X by A8;
      hence u in union a 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 being Subset of T such that
A9: a = A and
A10: A has_the_property_(S) by A1;
 assume b in the topology of T;
  then consider B being Subset of T such that
A11: b = B and
A12: B has_the_property_(S) by A1;
     A /\ B has_the_property_(S)
    proof let D be non empty directed Subset of T;
     assume
A13:   sup D in A /\ B;
      then sup D in A by XBOOLE_0:def 3;
      then consider x being Element of T such that
A14:    x in D and
A15:    for z being Element of T st z in D & z >= x holds z in A by A10,Def3;
        sup D in B by A13,XBOOLE_0:def 3;
      then consider y being Element of T such that
A16:    y in D and
A17:    for z being Element of T st z in D & z >= y holds z in B by A12,Def3;
      consider z being Element of T such that
A18:    z in D and
A19:    x <= z and
A20:   y <= z by A14,A16,WAYBEL_0:def 1;
     take z;
     thus z in D by A18;
     let u be Element of T such that
A21:   u in D;
     assume
A22:   u >= z;
      then u >= x by A19,YELLOW_0:def 2;
then A23:    u in A by A15,A21;
        u >= y by A20,A22,YELLOW_0:def 2;
      then u in B by A17,A21;
     hence u in A /\ B by A23,XBOOLE_0:def 3;
    end;
  hence a /\ b in the topology of T by A1,A9,A11;
end;

begin :: Scott Convergence

reserve R for non empty RelStr,
        N for net of R,
        i for Element of N;

definition let R,N;
 func lim_inf N -> Element of R equals
:Def6: "\/"({"/\"({N.i:i >= j},R) where j is Element of N:
           not contradiction},R);
 correctness;
end;

definition let R be reflexive non empty RelStr;
 let N be net of R, p be Element of R;
 pred p is_S-limit_of N means
:Def7: p <= lim_inf N;
end;

definition let R be reflexive non empty RelStr;
 func Scott-Convergence R -> Convergence-Class of R means
:Def8: for N being strict net of R st N in NetUniv R
 for p being 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 being strict net of R st N = $1 & $2 is_S-limit_of N;
    consider C being Relation of NetUniv R, the carrier of R such that
A1:   for x being Element of NetUniv R, y being Element of R
      holds [x,y] in C iff P[x,y] from Rel_On_Dom_Ex;
    reconsider C as Convergence-Class of R by YELLOW_6:def 21;
   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 being 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 p is_S-limit_of N implies [N,p] in C by A1,A2;
  end;
 uniqueness
  proof let it1,it2 be Convergence-Class of R such that
A3: for N being strict net of R st N in NetUniv R
    for p being Element of R
     holds [N,p] in it1 iff p is_S-limit_of N and
A4: for N being strict net of R st N in NetUniv R
    for p being Element of R
     holds [N,p] in it2 iff p is_S-limit_of N;
   let x,y be set;
A5:  it1 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 21;
A6:  it2 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 21;

   hereby assume
A7:  [x,y] in it1;
     then A8:    x in NetUniv R by A5,ZFMISC_1:106;
     then consider N being 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 14
;
     reconsider p = y as Element of R by A5,A7,ZFMISC_1:106;
       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:106;
    then consider N being 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 14;
    reconsider p = y as Element of R by A6,A10,ZFMISC_1:106;
      p is_S-limit_of N by A4,A10,A11,A12;
   hence [x,y] in it1 by A3,A11,A12;
  end;
end;

:: remarks, p.98

theorem
   for R being complete LATTICE,
     N being net of R, p,q being 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 being Element of N such that
A3: for i being Element of N st j0 <= i holds N.i in downarrow q
     by A2,WAYBEL_0:def 11;
  set X = {"/\"({N.i where i is Element of N:
             i >= j},R) where j is Element of N:
               not contradiction};
A4: lim_inf N = "\/"(X,R) by Def6;
  reconsider q'= q, p' = p as Element of R;
    q' is_>=_than X
   proof let x be Element of R;
    assume x in X;
     then consider j1 being Element of N such that
A5:  x = "/\"({N.i where i is Element of N: i >= j1},R);
     set Y = {N.i where i is Element of N: i >= j1};
     reconsider j1 as Element of N;
     consider j2 being Element of N such that
A6:   j2 >= j0 & j2 >= j1 by YELLOW_6:def 5;
       N.j2 in Y by A6;
     then A7:    x <= N.j2 by A5,YELLOW_2:24;
       N.j2 in downarrow q by A3,A6;
     then N.j2 <= q' by WAYBEL_0:17;
    hence x <= q' by A7,YELLOW_0:def 2;
   end;
  then lim_inf N <= q' by A4,YELLOW_0:32;
  then p' <= q' by A1,YELLOW_0:def 2;
 hence p <= q;
end;

theorem Th18:
 for R being complete LATTICE,
     N being net of R, p,q being 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 being Element of N such that
A1: for i being Element of N st j0 <= i holds N.i in uparrow q
     by WAYBEL_0:def 11;
  set X = {"/\"({N.i where i is Element of N:
             i >= j},R) where j is Element of N:
               not contradiction},
      Y = {N.i where i is Element of N: i >= j0};
A2: lim_inf N = "\/"(X,R) by Def6;
  reconsider q'= q as Element of R;
    "/\"(Y,R) in X;
  then A3: lim_inf N >= "/\"(Y,R) by A2,YELLOW_2:24;
    q' is_<=_than Y
   proof let y be Element of R;
    assume y in Y;
     then consider i1 being Element of N such that
A4:  y = N.i1 and
A5:  i1 >= j0;
     reconsider i1' = i1 as Element of N;
       N.i1' in uparrow q by A1,A5;
    hence q' <= y by A4,WAYBEL_0:18;
   end;
  then "/\"(Y,R) >= q' by YELLOW_0:33;
 hence lim_inf N >= q by A3,YELLOW_0:def 2;
end;

definition
 let R be reflexive non empty RelStr, N be non empty NetStr over R;
 redefine
  attr N is monotone means
:Def9: for i,j being 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 by WAYBEL_0:def 9;
    let i,j be Element of N;
A2:   netmap(N,R).i = (the mapping of N).i by WAYBEL_0:def 7
        .= N.i by WAYBEL_0:def 8;
A3:   netmap(N,R).j = (the mapping of N).j by WAYBEL_0:def 7
        .= N.j by WAYBEL_0:def 8;
     reconsider i' = i, j' = j as Element of N;
    assume i <= j;
     then netmap(N,R).i' <= netmap(N,R).j' by A1,WAYBEL_1:def 2;
    hence N.i <= N.j by A2,A3;
   end;
   assume
A4:   for i,j being Element of N st i <= j
    holds N.i <= N.j;
      netmap(N,R) is monotone
    proof let x,y be Element of N;
A5:     netmap(N,R).x = (the mapping of N).x by WAYBEL_0:def 7
        .= N.x by WAYBEL_0:def 8;
A6:     netmap(N,R).y = (the mapping of N).y by WAYBEL_0:def 7
        .= N.y by WAYBEL_0:def 8;
     assume x <= y;
     hence netmap(N,R).x <= netmap(N,R).y by A4,A5,A6;
    end;
   hence N is monotone by WAYBEL_0:def 9;
  end;
end;

definition let R be non empty RelStr;
 let S be non empty set, f be Function of S, the carrier of R;
 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 being 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 being Relation of S,S such that
A1:   for x,y being Element of S holds [x,y] in R iff P[x,y]
        from Rel_On_Dom_Ex;
   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;
A2:  f.y = N.j by WAYBEL_0:def 8;
      [x,y] in the InternalRel of N iff f.x <= f.y by A1;
   hence i <= j iff N.i <= N.j by A2,ORDERS_1:def 9,WAYBEL_0:def 8;
  end;
 uniqueness
  proof let it1,it2 be strict non empty NetStr over R such that
A3: the carrier of it1 = S and
A4: the mapping of it1 = f and
A5: for i,j being Element of it1 holds i <= j iff it1.i <= it1.j and
A6: the carrier of it2 = S and
A7: the mapping of it2 = f and
A8: for i,j being Element of it2 holds i <= j iff it2.i <= it2.j;
      the InternalRel of it1 = the InternalRel of it2
     proof let x,y be set;
      hereby assume
A9:      [x,y] in the InternalRel of it1;
        then A10:       x in S & y in S by A3,ZFMISC_1:106;
        then reconsider i=x, j=y as Element of it1 by A3;
        reconsider i'=x, j'=y as Element of it2 by A6,A10;
A11:      it1.i = f.i by A4,WAYBEL_0:def 8 .= it2.i' by A7,WAYBEL_0:def 8;
A12:      it1.j = f.j by A4,WAYBEL_0:def 8 .= it2.j' by A7,WAYBEL_0:def 8;
          i <= j by A9,ORDERS_1:def 9;
        then it2.i' <= it2.j' by A5,A11,A12;
        then i' <= j' by A8;
       hence [x,y] in the InternalRel of it2 by ORDERS_1:def 9;
      end;
      assume
A13:      [x,y] in the InternalRel of it2;
        then A14:       x in S & y in S by A6,ZFMISC_1:106;
        then reconsider i=x, j=y as Element of it2 by A6;
        reconsider i'=x, j'=y as Element of it1 by A3,A14;
A15:      it2.i = f.i by A7,WAYBEL_0:def 8 .= it1.i' by A4,WAYBEL_0:def 8;
A16:      it2.j = f.j by A7,WAYBEL_0:def 8 .= it1.j' by A4,WAYBEL_0:def 8;
          i <= j by A13,ORDERS_1:def 9;
        then it1.i' <= it1.j' by A8,A15,A16;
        then i' <= j' by A5;
       hence [x,y] in the InternalRel of it1 by ORDERS_1:def 9;
     end;
   hence it1 = it2 by A3,A4,A6,A7;
  end;
end;

theorem Th19:
 for L being non empty 1-sorted, N being non empty NetStr over L
  holds rng the mapping of N =
   { N.i where i is Element of N: not contradiction}
proof let L be non empty 1-sorted, N be non empty NetStr over L;
  set X = { N.i where i is Element of N: not contradiction};
A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
 thus rng the mapping of N c=
   { N.i where i is Element of N: not contradiction}
 proof let e be set;
  assume e in rng the mapping of N;
   then consider u being set such that
A2: u in dom the mapping of N and
A3: e = (the mapping of N).u by FUNCT_1:def 5;
   reconsider u as Element of N by A2,FUNCT_2:def 1;
     e = N.u by A3,WAYBEL_0:def 8;
  hence e in X;
 end;
 let e be set;
 assume e in X;
  then consider i being Element of N such that
A4: e = N.i;
    e = (the mapping of N).i by A4,WAYBEL_0:def 8;
 hence e in rng the mapping of N by A1,FUNCT_1:def 5;
end;

theorem Th20:
 for R being non empty RelStr,
     S being 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;
A2: f = the mapping of N by Def10;
  then rng f =
   { N.i where i is Element of N: not contradiction} by Th19;
  then N.x in rng f & N.y in rng f;
  then consider p being Element of R such that
A3: p in rng f and
A4: N.x <= p & N.y <= p by A1,WAYBEL_0:def 1;
   consider z being set such that
A5: z in dom f and
A6: p = f.z by A3,FUNCT_1:def 5;
    z in the carrier of N by A2,A5,FUNCT_2:def 1;
  then reconsider z as Element of N;
 take z;
    p = N.z by A2,A6,WAYBEL_0:def 8;
 hence x <= z & y <= z by A4,Def10;
end;

definition 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 = (the mapping of N).x by WAYBEL_0:def 7
        .= N.x by WAYBEL_0:def 8;
A2:   netmap(N,R).y = (the mapping of N).y by WAYBEL_0:def 7
        .= N.y by WAYBEL_0:def 8;
      assume x <= y;
      hence netmap(N,R).x <= netmap(N,R).y by A1,A2,Def10;
     end;
   hence thesis by WAYBEL_0:def 9;
  end;
end;

definition 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 x <= y & y <= z;
    then N.x <= N.y & N.y <= N.z by Def10;
    then N.x <= N.z by YELLOW_0:def 2;
   hence x <= z by Def10;
  end;
end;

definition 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 Th21:
 for R being non empty transitive RelStr,
     S being 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;
A3:  UN = Tarski-Class the_transitive-closure_of the carrier of R by YELLOW_6:
def 3;
      reconsider UN as universal set;
A4: the_transitive-closure_of the carrier of R in UN by A3,CLASSES1:5;
     the carrier of R c= the_transitive-closure_of the carrier of R
                         by CLASSES1:59;
   then the carrier of R in UN by A3,A4,CLASSES1:6;
then A5: S in UN by A1,CLASSES1:def 1;
    the carrier of N = S by Def10;
 hence Net-Str(S,f) in NetUniv R by A5,YELLOW_6:def 14;
end;

definition let R be LATTICE;
 cluster monotone reflexive strict 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 = the carrier of R by RELAT_1:71
         .= [#]R by PRE_TOPC:12;
    then reconsider N = Net-Str(the carrier of R,f) as strict reflexive net of
R
                                    by Th20;
   take N;
   thus thesis;
  end;
end;

theorem Th22:
 for R being complete LATTICE,
     N being monotone reflexive net of R
 holds lim_inf N = sup N
proof
 let R be complete LATTICE,
     N be monotone reflexive net of R;
  defpred P[set] means not contradiction;
  deffunc F(Element of N)
    = "/\"({N.i where i is Element of N: i >= $1},R);
  set X = {F(j) where j is Element of N: P[j]};
   deffunc G(Element of N) = N.$1;
A1: for j being Element of N holds G(j) = F(j)
   proof let j be Element of N;
     set Y = {N.i where i is 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 being Element of N st
          y = N.i & j <= i;
       hence N.j <= y by Def9;
      end;
       for b being 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 j' = j as Element of N;
          j' <= j';
        then N.j' in Y;
       hence N.j >= b by A3,LATTICE3:def 8;
      end;
    hence N.j = "/\"(Y,R) by A2,YELLOW_0:33;
   end;
    rng the mapping of N = { G(j) where j is Element of N: P[j]}
              by Th19
         .= X from FraenkelF'(A1);
 hence lim_inf N = "\/"(rng the mapping of N,R) by Def6
       .= Sup the mapping of N by YELLOW_2:def 5
       .= sup N by WAYBEL_2:def 1;
end;

theorem Th23:
 for R being complete LATTICE,
     N being 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 = {"/\"({N.i where i is Element of N:
             i >= j},R) where j is Element of N:
               not contradiction};
  consider j being Element of N;
A1: N.j is_>=_than X
   proof let b be Element of R;
    assume b in X;
     then consider j0 being Element of N such that
A2:   b = "/\"({N.i where i is Element of N: i >= j0},R);
     reconsider j0 as Element of N;
     consider i0 being Element of N such that
A3:   i0 >= j0 and i0 >= j0 by YELLOW_6:def 5;
A4:  N.i0 in {N.i where i is Element of N: i >= j0} by A3;
       N.i0 = the_value_of N by YELLOW_6:25
         .= N.j by YELLOW_6:25;
    hence N.j >= b by A2,A4,YELLOW_2:24;
   end;
A5: for b being 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 is Element of N: i >= j};
A6:    "/\"(Y,R) in X;
     assume b is_>=_than X;
then A7:       b >= "/\"(Y,R) by A6,LATTICE3:def 9;
A8:    N.j is_<=_than Y
       proof let c be Element of R;
        assume c in Y;
         then consider i0 being Element of N such that
A9:       c = N.i0 and i0 >= j;
           N.j = the_value_of N by YELLOW_6:25
            .= N.i0 by YELLOW_6:25;
        hence N.j <= c by A9;
       end;
        for b being Element of R st b is_<=_than Y holds N.j >= b
       proof let c be Element of R;
         consider i0 being Element of N such that
A10:       i0 >= j and i0 >= j by YELLOW_6:def 5;
A11:       N.i0 in Y by A10;
        assume
A12:      c is_<=_than Y;
           N.j = the_value_of N by YELLOW_6:25
            .= N.i0 by YELLOW_6:25;
        hence N.j >= c by A11,A12,LATTICE3:def 8;
       end;
     hence N.j <= b by A7,A8,YELLOW_0:33;
    end;
 thus the_value_of N = N.j by YELLOW_6:25
        .= "\/"(X,R) by A1,A5,YELLOW_0:32
        .= lim_inf N by Def6;
end;

theorem Th24:
 for R being complete LATTICE,
     N being constant net of R
  holds the_value_of N is_S-limit_of N
proof
 let R be complete LATTICE,
     N be constant net of R;
    the_value_of N <= lim_inf N by Th23;
 hence the_value_of N is_S-limit_of N by Def7;
end;

definition let S be non empty 1-sorted, e be Element of S;
 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:8;
    dom id{e} = {e} & rng id{e} = {e} by RELAT_1:71;
    then reconsider f = id{e} as Function of {e}, the carrier of S
       by FUNCT_2:def 1,RELSET_1:11;
   take NetStr(#{e},r,f#);
   thus thesis;
  end;
 uniqueness;
end;

definition 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 Th25:
 for S being non empty 1-sorted, e being Element of S,
     x being 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;
     x in the carrier of Net-Str e & the carrier of Net-Str e = {e} by Def11;
  hence thesis by TARSKI:def 1;
 end;

theorem Th26:
 for S being non empty 1-sorted, e being Element of S,
     x being 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: x in the carrier of Net-Str e & the carrier of Net-Str e = {e} by Def11;
   then A2:  x = e by TARSKI:def 1;
  thus N.x = (the mapping of N).x by WAYBEL_0:def 8
          .= (id{e}).x by Def11
          .= e by A1,A2,FUNCT_1:35;
 end;

definition 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;
A1:  the carrier of N = {e} by Def11;
      e in {e} by TARSKI:def 1;
    then reconsider e as Element of N by A1;
      the InternalRel of N = {[e,e]} by Def11;
    then A2:  [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 x <= x by A2,ORDERS_1:def 9;
    end;
   thus N is transitive
    proof let x,y,z be Element of N such that x <= y & y <= z;
        x = e & z = e by Th25;
     hence thesis by A2,ORDERS_1:def 9;
    end;
   thus N is directed
    proof let x,y be Element of N;
     take e;
        x = e & y = e by Th25;
     hence thesis by A2,ORDERS_1:def 9;
    end;
   let x,y be Element of N such that x <= y & y <= x;
      x = e & y = e by Th25;
   hence thesis;
  end;
end;

theorem Th27:
 for S being non empty 1-sorted, e being Element of S,
     X being 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;
A1:  the carrier of N = {e} by Def11;
      e in {e} by TARSKI:def 1;
    then reconsider d = e as Element of N by A1;
 hereby assume N is_eventually_in X;
   then consider x being Element of N such that
A2:  for y being Element of N st x <= y holds N.y in X by WAYBEL_0:def 11;
     N.x in X by A2;
  hence e in X by Th26;
 end;
 assume
A3: e in X;
  take d;
 let j be Element of N such that d <= j;
 thus N.j in X by A3,Th26;
end;

theorem Th28:
 for S being reflexive antisymmetric (non empty RelStr),
     e being 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 = {"/\"({N.i where i is Element of N:
             i >= j},S) where j is Element of N:
              not contradiction};
  reconsider e' = e as Element of S;
A1: X c= {e'}
   proof let u be set;
    assume u in X;
     then consider j being Element of N such that
A2:    u = "/\"({N.i where i is Element of N: i >= j},S);
     set Y = {N.i where i is Element of N: i >= j};
A3:   Y c= {e'}
      proof let v be set;
       assume v in Y;
        then consider i being Element of N such that
A4:      v = N.i and i >= j;
        reconsider i' = i as Element of N;
          N.i' = e by Th26;
       hence v in {e'} by A4,TARSKI:def 1;
      end;
     reconsider j' = j as Element of N;
       j' <= j';
     then N.j in Y;
     then Y = {e'} by A3,ZFMISC_1:39;
     then u = e' by A2,YELLOW_0:39;
    hence u in {e'} by TARSKI:def 1;
   end;
  consider j being Element of N;
    "/\"({N.i where i is Element of N: i >= j},S) in X;
  then X = {e'} by A1,ZFMISC_1:39;
 hence e = "\/"(X,S) by YELLOW_0:39
    .= lim_inf Net-Str e by Def6;
end;

theorem Th29:
 for S being non empty reflexive RelStr,
     e being 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} & e in the carrier of S by Def11;
A2:  UN = Tarski-Class the_transitive-closure_of the carrier of S by YELLOW_6:
def 3;
      reconsider UN as universal set;
A3: the_transitive-closure_of the carrier of S in UN by A2,CLASSES1:5;
     the carrier of S c= the_transitive-closure_of the carrier of S
                         by CLASSES1:59;
   then the carrier of S in UN by A2,A3,CLASSES1:6;
   then the carrier of N in the_universe_of the carrier of S by A1,CLASSES1:def
1;
  hence Net-Str e in NetUniv S by YELLOW_6:def 14;
 end;

theorem Th30:
 for R being complete LATTICE, Z be net of R, D be Subset of R st
  D = {"/\"({Z.k where k is Element of Z: k >= j},R)
            where j is Element of Z: not contradiction}
  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 = {"/\"({Z.k where k is Element of Z: k >= j},R)
            where j is Element of Z: not contradiction};
  consider j being Element of Z;
    "/\"({Z.k where k is 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 being Element of Z such that
A2: x = "/\"({Z.k where k is Element of Z: k >= jx},R) by A1;
 assume y in D;
  then consider jy being Element of Z such that
A3: y = "/\"({Z.k where k is Element of Z: k >= jy},R) by A1;
  reconsider jx, jy as Element of Z;
  consider j being Element of Z such that
A4: j >= jx and
A5: j >= jy by YELLOW_6:def 5;
  set E1 = {Z.k where k is Element of Z: k >= jx},
      Ey = {Z.k where k is Element of Z: k >= jy},
      E = {Z.k where k is Element of Z: k >= j};
 take z = "/\"({Z.k where k is Element of Z: k >= j},R);
 thus z in D by A1;
    E c= E1
   proof let e be set;
    assume e in E;
     then consider k being 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 e in E1 by A6;
   end;
 hence x <= z by A2,WAYBEL_7:3;
    E c= Ey
   proof let e be set;
    assume e in E;
     then consider k being 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 e in Ey by A8;
   end;
 hence y <= z by A3,WAYBEL_7:3;
end;

theorem Th31: :: 1.2. Lemma, p.99
 for L being complete LATTICE
 for S being 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 is Subset of L:
      for p being Element of L st p in V
       for N being net of L st [N,p] in SC holds N is_eventually_in V}
         by YELLOW_6:def 27;
   let S be Subset of L;
   hereby assume S in the topology of T;
     then consider V being Subset of L such that
A2:   S = V and
A3:   for p being Element of L st p in V
       for N being 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
A4:    sup D in S;
A5:     dom id D = D & rng id D = D by RELAT_1:71;
       then reconsider f = id D as Function of D, the carrier of L
                                       by FUNCT_2:def 1,RELSET_1:11;
       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:71;
       then sup D is_S-limit_of N by Def7;
       then [N,sup D] in SC by A6,Def8;
       then N is_eventually_in S by A2,A3,A4;
       then consider i0 being Element of N such that
A7:     for j being Element of N st i0 <= j holds N.j in S by WAYBEL_0:def 11;
       consider j0 being Element of N such that
A8:     j0 >= i0 and j0 >= i0 by YELLOW_6:def 5;
A9:    N.j0 in S by A7,A8;
A10:     D = the carrier of N by Def10;
         N.j0 = (the mapping of N).j0 by WAYBEL_0:def 8
           .= (id D).j0 by Def10
           .= j0 by A10,FUNCT_1:35;
      hence D meets S 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,Def7;
       then [Net-Str y,x] in SC by A13,Def8;
       then Net-Str y is_eventually_in S by A2,A3,A11;
      hence y in S by Th27;
     end;
   end;
   assume that
A14: S is inaccessible and
A15: S is upper;
      for p being Element of L st p in S
     for N being 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 p' = 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 21;
       then A18:     N in NetUniv L by A17,ZFMISC_1:106;
     then ex N' being strict net of L st N' = N &
       the carrier of N' in
 the_universe_of the carrier of L by YELLOW_6:def 14;
       then p is_S-limit_of N by A17,A18,Def8;
       then A19:      p' <= lim_inf N by Def7;
       defpred P[set] means not contradiction;
       deffunc F(Element of N)
         = "/\"({N.i where i is Element of N: i >= $1},L);
       set X ={F(j) where j is Element of N: P[j]};
         X is Subset of L from SubsetFD;
       then reconsider D = X as Subset of L;
       reconsider D as non empty directed Subset of L by Th30;
         lim_inf N = sup D by Def6;
       then sup D in S by A15,A16,A19,WAYBEL_0:def 20;
       then D meets S by A14,Def1;
       then D /\ S <> {} by XBOOLE_0:def 7;
       then consider d being Element of L such that
A20:     d in D /\ S by SUBSET_1:10;
       reconsider d as Element of L;
         d in D by A20,XBOOLE_0:def 3;
       then consider j being Element of N such that
A21:   d = "/\"({N.i where i is 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 3;
      assume j <= i0;
       then N.i0 in {N.i where i is Element of N: i >= j};
       then d <= N.i0 by A21,YELLOW_2:24;
      hence N.i0 in S by A15,A22,WAYBEL_0:def 20;
     end;
   hence S in the topology of T by A1;
  end;

theorem Th32:
 for T being 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;
A1: the carrier of T = the carrier of CSC by YELLOW_6:def 27;
     the topology of T = the topology of CSC
    proof
     thus the topology of T c= the topology of CSC
      proof let e be set;
       assume
A2:      e in the topology of T;
        then reconsider A = e as Subset of T;
          A is open by A2,PRE_TOPC:def 5;
        then A is inaccessible upper by Def4;
       hence e in the topology of CSC by Th31;
      end;
     let e be set;
     assume
A3:    e in the topology of CSC;
      then reconsider A = e as Subset of T by A1;
        A is inaccessible upper by A3,Th31;
      then A is open by Def4;
     hence e in the topology of T by PRE_TOPC:def 5;
    end;
 hence the TopStruct of T = ConvergenceSpace Scott-Convergence T
    by YELLOW_6:def 27;
end;

theorem Th33:
 for T being complete TopLattice
  st the TopStruct of T = ConvergenceSpace Scott-Convergence T
 for S being 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 is Subset of T:
      for p being Element of T st p in V
       for N being net of T st [N,p] in SC holds N is_eventually_in V}
         by YELLOW_6:def 27;
   let S be Subset of T;
   hereby assume S is open;
     then S in the topology of T by PRE_TOPC:def 5;
     then consider V being Subset of T such that
A2:   S = V and
A3:   for p being Element of T st p in V
       for N being 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
A4:    sup D in S;
A5:     dom id D = D & rng id D = D by RELAT_1:71;
       then reconsider f = id D as Function of D, the carrier of T
                                       by FUNCT_2:def 1,RELSET_1:11;
       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:71;
       then sup D is_S-limit_of N by Def7;
       then [N,sup D] in SC by A6,Def8;
       then N is_eventually_in S by A2,A3,A4;
       then consider i0 being Element of N such that
A7:     for j being Element of N st i0 <= j holds N.j in S by WAYBEL_0:def 11;
       consider j0 being Element of N such that
A8:     j0 >= i0 and j0 >= i0 by YELLOW_6:def 5;
A9:    N.j0 in S by A7,A8;
A10:     D = the carrier of N by Def10;
         N.j0 = (the mapping of N).j0 by WAYBEL_0:def 8
           .= (id D).j0 by Def10
           .= j0 by A10,FUNCT_1:35;
      hence D meets S 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,Def7;
       then [Net-Str y,x] in SC by A13,Def8;
       then Net-Str y is_eventually_in S by A2,A3,A11;
      hence y in S by Th27;
     end;
   end;
   assume that
A14: S is inaccessible and
A15: S is upper;
      for p being Element of T st p in S
     for N being 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 p' = 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 21;
       then A18:     N in NetUniv T by A17,ZFMISC_1:106;
     then ex N' being strict net of T st N' = N &
       the carrier of N' in
 the_universe_of the carrier of T by YELLOW_6:def 14;
       then p is_S-limit_of N by A17,A18,Def8;
       then A19:      p' <= lim_inf N by Def7;
       defpred P[set] means not contradiction;
       deffunc F(Element of N)
         = "/\"({N.i where i is Element of N: i >= $1},T);
       set X ={F(j) where j is Element of N: P[j]};
         X is Subset of T from SubsetFD;
       then reconsider D = X as Subset of T;
       reconsider D as non empty directed Subset of T by Th30;
         lim_inf N = sup D by Def6;
       then sup D in S by A15,A16,A19,WAYBEL_0:def 20;
       then D meets S by A14,Def1;
       then D /\ S <> {} by XBOOLE_0:def 7;
       then consider d being Element of T such that
A20:     d in D /\ S by SUBSET_1:10;
       reconsider d as Element of T;
         d in D by A20,XBOOLE_0:def 3;
       then consider j being Element of N such that
A21:   d = "/\"({N.i where i is 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 3;
      assume j <= i0;
       then N.i0 in {N.i where i is Element of N: i >= j};
       then d <= N.i0 by A21,YELLOW_2:24;
      hence N.i0 in S by A15,A22,WAYBEL_0:def 20;
     end;
    then S in the topology of T by A1;
   hence S is open by PRE_TOPC:def 5;
  end;

theorem Th34:
 for T being complete TopLattice
   st the TopStruct of T = ConvergenceSpace Scott-Convergence T
  holds T is Scott
  proof let T be complete TopLattice;
   assume the TopStruct of T = ConvergenceSpace Scott-Convergence T;
   hence for S being Subset of T holds S is open iff S is inaccessible upper
           by Th33;
  end;

definition let R be complete LATTICE;
  :: 1.6. Proposition (i)
 cluster Scott-Convergence R -> (CONSTANTS);
 coherence
  proof
    let N be constant net of R;
     assume
A1:    N in NetUniv R;
      then consider M being 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 14;
         the_value_of M is_S-limit_of M by A2,Th24;
     hence [N,the_value_of N] in Scott-Convergence R by A1,A2,Def8;
  end;
end;

definition let R be complete LATTICE;
  :: 1.6. Proposition (i)
 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 21;
   assume
A2:  Y in NetUniv R;
   then consider Y' being strict net of R such that
A3:  Y' = Y and the carrier of Y' in the_universe_of the carrier of R
       by YELLOW_6:def 14;
   let p be Element of R;
    reconsider p' = p as Element of R;
   assume
A4: [N,p] in S;
   then A5: N in NetUniv R by A1,ZFMISC_1:106;
   then consider N' being strict net of R such that
A6:  N' = N and the carrier of N' in the_universe_of the carrier of R
       by YELLOW_6:def 14;
    deffunc F(Element of N)
     = "/\"({N.i where i is Element of N: i >= $1},R);
    defpred P[set] means not contradiction;
    reconsider X1 = {F(j) where j is Element of N: P[j]}
     as Subset of R from SubsetFD;
    deffunc G(Element of Y)
     = "/\"({Y.i where i is Element of Y: i >= $1},R);
    reconsider X2 = {G(j) where j is Element of Y: P[j]}
             as Subset of R from SubsetFD;
      p is_S-limit_of N' by A4,A5,A6,Def8;
    then p <= lim_inf N by A6,Def7;
    then A7:   p' <= "\/"(X1,R) by Def6;
    consider f being map of Y, N such that
A8:  the mapping of Y = (the mapping of N)*f and
A9:  for m being Element of N ex n being Element of Y st
      for p being Element of Y st n <= p holds m <= f.p by YELLOW_6:def 12;
      X1 is_finer_than X2
     proof let a be Element of R;
      assume a in X1;
       then consider j being Element of N such that
A10:    a = "/\"({N.i where i is Element of N: i >= j},R);
       reconsider j as Element of N;
       consider n being Element of Y such that
A11:     for p being Element of Y st n <= p holds j <= f.p by A9;
       set X3 = {Y.i where i is Element of Y: i >= n},
           X4 = {N.i where i is Element of N: i >= j};
      take b = "/\"(X3,R);
      thus b in X2;
         X3 c= X4
        proof let u be set;
         assume u in X3;
          then consider m being 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 = ((the mapping of N)*f).m by A8,A12,WAYBEL_0:def 8
           .= (the mapping of N).(f.m) by FUNCT_2:21
           .= N.(f.m) by WAYBEL_0:def 8;
         hence u in X4 by A14;
        end;
      hence a <= b by A10,WAYBEL_7:3;
     end;
    then "\/"(X1,R) <= "\/"(X2,R) by Th2;
    then p' <= "\/"(X2,R) by A7,YELLOW_0:def 2;
    then p <= lim_inf Y by Def6;
    then p is_S-limit_of Y' by A3,Def7;
   hence [Y,p] in S by A2,A3,Def8;
  end;
end;

theorem Th35: :: YELLOW_6:32
 for S being non empty 1-sorted, N being net of S, X being set
 for M being subnet of N st M = N"X
 for i being 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 13;
  then A2: (the mapping of N).j in X by FUNCT_1:def 13;
    the mapping of M = (the mapping of N)|the carrier of M by A1,YELLOW_6:def 8
;
  then (the mapping of M).j in X by A2,FUNCT_1:72;
 hence M.j in X by WAYBEL_0:def 8;
end;

definition let L be non empty reflexive RelStr;
 func sigma L -> Subset-Family of L equals
:Def12: the topology of ConvergenceSpace Scott-Convergence L;
 coherence by YELLOW_6:def 27;
end;

theorem Th36: :: 1.5 Examples (5), p.100
 for L being 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 being Element of L such that
A1:    d in D and
A2:    x << d by WAYBEL_4:54;
       d in W by A2,WAYBEL_3:8;
    hence D meets W by A1,XBOOLE_0:3;
   end;
 hence wayabove x is open by Def4;
end;

theorem Th37:
 for T being complete TopLattice
   st the topology of T = sigma T
  holds T is Scott
proof let T be complete TopLattice;
A1:  sigma T = the topology of ConvergenceSpace Scott-Convergence T by Def12;
 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 A1,YELLOW_6:def 27;
 hence thesis by Th34;
end;

:: non automated structural loci :

Lm3:
 for T1,T2 being TopStruct
  st the TopStruct of T1 = the TopStruct of T2 & T1 is TopSpace-like
  holds T2 is TopSpace-like
proof
 let T1,T2 be TopStruct such that
A1: the TopStruct of T1 = the TopStruct of T2 and
A2: T1 is TopSpace-like;
 thus the carrier of T2 in the topology of T2 by A1,A2,PRE_TOPC:def 1;
 thus (for a being Subset-Family of T2
      st a c= the topology of T2
       holds union a in the topology of T2) &
     (for a,b being Subset of T2 st
      a in the topology of T2 & b in the topology of T2
       holds a /\ b in the topology of T2) by A1,A2,PRE_TOPC:def 1;
end;

Lm4:
 for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2
 for N being strict net of S1 holds N is strict net of S2
proof
 let S1,S2 be non empty 1-sorted such that
A1: the carrier of S1 = the carrier of S2;
 let N be strict net of S1;
  reconsider M = N as net of S2 by A1;
A2: the carrier of N = the carrier of M &
   the InternalRel of N = the InternalRel of M &
   the mapping of N = the mapping of M;
    M = the NetStr of N
   .= the NetStr of M by A2;
 hence N is strict net of S2;
end;

Lm5:
 for S1,S2 being 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 being 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 being strict net of S1 such that
A3:    N = x & the carrier of N in the_universe_of the carrier of S1
        by YELLOW_6:def 14;
     reconsider N as strict net of S2 by A1,Lm4;
     thus P[x] proof take N; thus thesis by A1,A3; end;
    end;
    assume P[x]; then consider N being strict net of S2 such that
A4:   N = x & the carrier of N in the_universe_of the carrier of S2;
     reconsider N as strict net of S1 by A1,Lm4;
       now take N;
       thus N = x & the carrier of N in the_universe_of the carrier of S1
         by A1,A4;
     end;
    hence x in NetUniv S1 by YELLOW_6:def 14;
   end;
A5: for x being set holds x in NetUniv S2 iff P[x] by YELLOW_6:def 14;
 thus NetUniv S1 = NetUniv S2 from Extensionality(A2,A5);
end;

Lm6:
 for T1,T2 being non empty 1-sorted, X be set
  st the carrier of T1 = the carrier of T2
 for N1 being net of T1, N2 being 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 such that
      the carrier of T1 = the carrier of T2;
 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 being Element of N1 such that
A2:   for j being Element of N1 st i <= j holds N1.j in X by WAYBEL_0:def 11;
     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 = (the mapping of N2).jj by WAYBEL_0:def 8
          .= (the mapping of N1).j by A1
          .= N1.j by WAYBEL_0:def 8;
    hence N2.jj in X by A1,A2,A3;
end;

Lm7:
 for T1,T2 being non empty TopSpace
  st the TopStruct of T1 = the TopStruct of T2
 for N1 being net of T1, N2 being net of T2 st N1 = N2
 for p1 being Point of T1, p2 being 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 being 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 being Subset of T2 such that
A5:   G is open and
A6:   G c= V and
A7:   p2 in G by TOPS_1:54;
     reconsider H = G as Subset of T1 by A1;
       G in the topology of T2 by A5,PRE_TOPC:def 5;
     then H is open by A1,PRE_TOPC:def 5;
     then p1 in Int W by A3,A6,A7,TOPS_1:54;
     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 18;
      then consider i being Element of N1 such that
A8:    for j being Element of N1 st i <= j holds N1.j in W by WAYBEL_0:def 11;
      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 = (the mapping of N2).jj by WAYBEL_0:def 8
           .= (the mapping of N1).j by A2
           .= N1.j by WAYBEL_0:def 8;
      hence N2.jj in V by A2,A8,A9;
     end;
   end;
 hence p2 in Lim N2 by YELLOW_6:def 18;
end;

Lm8:
 for T1,T2 being 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 21;
A3: Convergence T2 c= [:NetUniv T2,the carrier of T2:] by YELLOW_6:def 21;
  let u1,u2 be set;
   hereby assume
A4:  [u1,u2] in Convergence T1;
    then consider N1 being Element of NetUniv T1, p1 being Point of T1
    such that
A5:  [u1,u2] = [N1,p1] by A2,DOMAIN_1:9;
A6:  N1 in NetUniv T1;
      ex N being strict net of T1 st N = N1 &
     the carrier of N in the_universe_of the carrier of T1 by YELLOW_6:def 14;
    then reconsider N1 as net of T1;
A7:  p1 in Lim N1 by A4,A5,YELLOW_6:def 22;
    reconsider N2 = N1 as net of T2 by A1;
    reconsider p2 =p1 as Point of T2 by A1;
      N2 in NetUniv T2 & p2 in Lim N2 by A1,A6,A7,Lm5,Lm7;
   hence [u1,u2] in Convergence T2 by A5,YELLOW_6:def 22;
   end;
   assume
A8: [u1,u2] in Convergence T2;
    then consider N1 being Element of NetUniv T2, p1 being Point of T2
    such that
A9:  [u1,u2] = [N1,p1] by A3,DOMAIN_1:9;
A10:  N1 in NetUniv T2;
      ex N being strict net of T2 st N = N1 &
     the carrier of N in the_universe_of the carrier of T2 by YELLOW_6:def 14;
    then reconsider N1 as net of T2;
A11:  p1 in Lim N1 by A8,A9,YELLOW_6:def 22;
    reconsider N2 = N1 as net of T1 by A1;
    reconsider p2 =p1 as Point of T1 by A1;
      N2 in NetUniv T1 & p2 in Lim N2 by A1,A10,A11,Lm5,Lm7;
   hence [u1,u2] in Convergence T1 by A9,YELLOW_6:def 22;
end;

Lm9:
 for R1,R2 being 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 x' = x, y' = y as Element of R1 by A1;
      consider z' being Element of R1 such that
A4:    z' <= x' & z' <= y' and
A5:    for w' being Element of R1 st w' <= x' & w' <= y' holds w' <= z'
                      by A2,LATTICE3:def 11;
      reconsider z = z' as Element of R2 by A1;
     take z;
     thus z <= x & z <= y by A1,A4,Lm1;
     let w be Element of R2;
      reconsider w' = w as Element of R1 by A1;
     assume w <= x & w <= y;
      then w' <= x' & w' <= y' by A1,Lm1;
      then w' <= z' by A5;
     hence w <= z by A1,Lm1;
    end;
A6: R2 is with_suprema
    proof let x,y be Element of R2;
      reconsider x' = x, y' = y as Element of R1 by A1;
      consider z' being Element of R1 such that
A7:    z' >= x' & z' >= y' and
A8:    for w' being Element of R1 st w' >= x' & w' >= y' holds w' >= z'
                      by A2,LATTICE3:def 10;
      reconsider z = z' as Element of R2 by A1;
     take z;
     thus z >= x & z >= y by A1,A7,Lm1;
     let w be Element of R2;
      reconsider w' = w as Element of R1 by A1;
     assume w >= x & w >= y;
      then w' >= x' & w' >= y' by A1,Lm1;
      then w' >= z' by A8;
     hence w >= z by A1,Lm1;
    end;
A9: R2 is reflexive
    proof let x be Element of R2;
      reconsider x' = x as Element of R1 by A1;
        x' <= x' by A2,YELLOW_0:def 1;
     hence x <= x by A1,Lm1;
    end;
A10: R2 is transitive
    proof let x,y,z be Element of R2;
      reconsider x' = x, y' = y, z' = z as Element of R1 by A1;
     assume x <= y & y <= z;
      then x' <= y' & y' <= z' by A1,Lm1;
      then x' <= z' by A2,YELLOW_0:def 2;
     hence x <= z by A1,Lm1;
    end;
     R2 is antisymmetric
    proof let x,y be Element of R2;
      reconsider x' = x, y' = y as Element of R1 by A1;
     assume x <= y & y <= x;
      then x' <= y' & y' <= x' by A1,Lm1;
     hence x = y by A2,YELLOW_0:def 3;
    end;
 hence thesis by A3,A6,A9,A10;
end;

Lm10:
 for R1,R2 being LATTICE, X being set
  st the RelStr of R1 = the RelStr of R2
 for p1 being Element of R1, p2 being Element of R2 st
  p1 = p2 & X is_<=_than p1
 holds X is_<=_than p2
proof
 let R1,R2 be LATTICE, X be set such that
A1: the RelStr of R1 = the RelStr of R2;
 let p1 be Element of R1, p2 be Element of R2 such that
A2: p1 = p2 and
A3: X is_<=_than p1;
 let b2 be Element of R2;
  reconsider b1 = b2 as Element of R1 by A1;
 assume b2 in X;
  then p1 >= b1 by A3,LATTICE3:def 9;
 hence p2 >= b2 by A1,A2,Lm1;
end;

Lm11:
 for R1,R2 being LATTICE, X being set
  st the RelStr of R1 = the RelStr of R2
 for p1 being Element of R1, p2 being Element of R2 st
  p1 = p2 & X is_>=_than p1
 holds X is_>=_than p2
proof
 let R1,R2 be LATTICE, X be set such that
A1: the RelStr of R1 = the RelStr of R2;
 let p1 be Element of R1, p2 be Element of R2 such that
A2: p1 = p2 and
A3: X is_>=_than p1;
 let b2 be Element of R2;
  reconsider b1 = b2 as Element of R1 by A1;
 assume b2 in X;
  then p1 <= b1 by A3,LATTICE3:def 8;
 hence p2 <= b2 by A1,A2,Lm1;
end;

Lm12:
 for R1,R2 being complete LATTICE
  st the RelStr of R1 = the RelStr of R2
 for D being 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 being Element of R2 st D is_<=_than a holds a >= b
   proof let a be Element of R2;
     reconsider a' = a as Element of R1 by A1;
    assume D is_<=_than a;
     then D is_<=_than a' by A1,Lm10;
     then a' >= "\/"(D,R1) by A3,YELLOW_0:def 9;
    hence a >= b by A1,Lm1;
   end;
 hence "\/"(D,R1) = "\/"(D,R2) by A2,A4,YELLOW_0:def 9;
end;

Lm13:
 for R1,R2 being complete LATTICE
  st the RelStr of R1 = the RelStr of R2
 for D being 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 being Element of R2 st D is_>=_than a holds a <= b
   proof let a be Element of R2;
     reconsider a' = a as Element of R1 by A1;
    assume D is_>=_than a;
     then D is_>=_than a' by A1,Lm11;
     then a' <= "/\"(D,R1) by A3,YELLOW_0:def 10;
    hence a <= b by A1,Lm1;
   end;
 hence "/\"(D,R1) = "/\"(D,R2) by A2,A4,YELLOW_0:def 10;
end;

Lm14:
 for R1,R2 being non empty reflexive RelStr
  st the RelStr of R1 = the RelStr of R2
 for D being Subset of R1, D' being Subset of R2 st D = D' & D is directed
  holds D' 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, D' be Subset of R2 such that
A2: D = D' and
A3: D is directed;
  let x2,y2 be Element of R2 such that
A4: x2 in D' & y2 in D';
   reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
   consider z1 being Element of R1 such that
A5: z1 in D and
A6:  x1 <= z1 & y1 <= z1 by A2,A3,A4,WAYBEL_0:def 1;
   reconsider z2 = z1 as Element of R2 by A1;
  take z2;
  thus z2 in D' by A2,A5;
  thus x2 <= z2 & y2 <= z2 by A1,A6,Lm1;
end;

Lm15:
 for R1,R2 being complete LATTICE
  st the RelStr of R1 = the RelStr of R2
 for p,q being Element of R1 st p << q
 for p',q' being Element of R2 st p = p' & q = q'
  holds p' << q'
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 p',q' be Element of R2 such that
A3: p = p' & q = q';
 let D' be non empty directed Subset of R2 such that
A4: q' <= sup D';
  reconsider D = D' as non empty Subset of R1 by A1;
  reconsider D as non empty directed Subset of R1 by A1,Lm14;
    sup D = sup D' by A1,Lm12;
  then q <= sup D by A1,A3,A4,Lm1;
  then consider d be Element of R1 such that
A5:  d in D & p <= d by A2,WAYBEL_3:def 1;
  reconsider d' = d as Element of R2 by A1;
 take d';
 thus d' in D' by A5;
 thus p' <= d' by A1,A3,A5,Lm1;
end;

Lm16:
 for R1,R2 being complete LATTICE
  st the RelStr of R1 = the RelStr of R2
 for N1 being net of R1, N2 being 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 = {"/\"({N1.i where i is Element of N1:
            i >= j},R1) where j is Element of N1:
           not contradiction},
      X2 = {"/\"({N2.i where i is Element of N2:
            i >= j},R2) where j is Element of N2:
           not contradiction};
A3: X1 = X2
  proof
   thus X1 c= X2
    proof let e be set;
     assume e in X1;
      then consider j1 being Element of N1 such that
A4:    e = "/\"({N1.i where i is Element of N1:
            i >= j1},R1);
      reconsider j2 = j1 as Element of N2 by A2;
      set Y1 = {N1.i where i is Element of N1: i >= j1},
          Y2 = {N2.i where i is Element of N2: i >= j2};
        Y1 = Y2
       proof
        thus Y1 c= Y2
         proof let u be set;
          assume u in Y1;
           then consider i1 being Element of N1 such that
A5:        u = N1.i1 and
A6:        j1 <= i1;
           reconsider i2 = i1 as Element of N2 by A2;
             N2.i2 = (the mapping of N2).i2 by WAYBEL_0:def 8
           .= (the mapping of N1).i1 by A2
           .= u by A5,WAYBEL_0:def 8;
          hence u in Y2 by A2,A6;
         end;
       let u be set;
        assume u in Y2;
         then consider i2 being Element of N2 such that
A7:      u = N2.i2 and
A8:      j2 <= i2;
         reconsider i1 = i2 as Element of N1 by A2;
           N1.i1 = (the mapping of N1).i1 by WAYBEL_0:def 8
           .= (the mapping of N2).i2 by A2
           .= u by A7,WAYBEL_0:def 8;
        hence u in Y1 by A2,A8;
       end;
      then e = "/\"(Y2,R2) by A1,A4,Lm13;
     hence e in X2;
    end;
   let e be set;
     assume e in X2;
      then consider j1 being Element of N2 such that
A9:    e = "/\"({N2.i where i is Element of N2:
            i >= j1},R2);
      reconsider j2 = j1 as Element of N1 by A2;
      set Y1 = {N2.i where i is Element of N2: i >= j1},
          Y2 = {N1.i where i is Element of N1: i >= j2};
        Y1 = Y2
       proof
        thus Y1 c= Y2
         proof let u be set;
          assume u in Y1;
           then consider i1 being Element of N2 such that
A10:        u = N2.i1 and
A11:        j1 <= i1;
           reconsider i2 = i1 as Element of N1 by A2;
             N1.i2 = (the mapping of N1).i2 by WAYBEL_0:def 8
           .= (the mapping of N2).i1 by A2
           .= u by A10,WAYBEL_0:def 8;
          hence u in Y2 by A2,A11;
         end;
       let u be set;
        assume u in Y2;
         then consider i2 being Element of N1 such that
A12:      u = N1.i2 and
A13:      j2 <= i2;
         reconsider i1 = i2 as Element of N2 by A2;
           N2.i1 = (the mapping of N2).i1 by WAYBEL_0:def 8
           .= (the mapping of N1).i2 by A2
           .= u by A12,WAYBEL_0:def 8;
        hence u in Y1 by A2,A13;
       end;
      then e = "/\"(Y2,R1) by A1,A9,Lm13;
     hence e in X1;
  end;
 thus lim_inf N1 = "\/"(X1,R1) by Def6
         .= "\/"(X2,R2) by A1,A3,Lm12
         .= lim_inf N2 by Def6;
end;

Lm17:
 for R1,R2 being non empty reflexive RelStr, X being non empty set
  st the RelStr of R1 = the RelStr of R2
 for N1 being net of R1, N2 being net of R2 st N1 = N2
 for J1 being net_set of the carrier of N1,R1,
     J2 being 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 such that
      the RelStr of R1 = the RelStr of R2;
  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 16;
A4: the RelStr of Iterated J2 = [:N2, product J2:]
                     by YELLOW_6:def 16;
then A5: the carrier of Iterated J1 = the carrier of Iterated J2 by A1,A2,A3;
A6: the InternalRel of Iterated J1 = the InternalRel of Iterated J2
          by A1,A2,A3,A4;
   set f = the mapping of Iterated J1, g = the mapping of Iterated J2;
A7: 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 being set st x in dom f holds f.x = g.x
    proof let x be set;
     assume x in dom f;
      then x in the carrier of Iterated J1 by FUNCT_2:def 1;
      then x in [:the carrier of N1, the carrier of product J1:]
                                        by A3,YELLOW_3:def 2;
      then consider x1 being Element of N1,
                    x2 being Element of product J1 such that
A8:    x = [x1,x2] by DOMAIN_1:9;
      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 A8,BINOP_1:def 1
        .= (the mapping of J1.x1).(x2.x1) by YELLOW_6:def 16
        .= (the mapping of J2.y1).(y2.y1) by A2
        .= (the mapping of Iterated J2).(y1,y2) by YELLOW_6:def 16
        .= g.x by A8,BINOP_1:def 1;
    end;
then A9: f = g by A7,FUNCT_1:9;
  thus Iterated J1 = NetStr(#the carrier of Iterated J1,
       the InternalRel of Iterated J1, the mapping of Iterated J1#)
      .= NetStr(#the carrier of Iterated J2,
       the InternalRel of Iterated J2, the mapping of Iterated J2#) by A5,A6,A9
      .= Iterated J2;
 end;

Lm18:
 for R1,R2 being non empty reflexive RelStr, X being non empty set
  st the RelStr of R1 = the RelStr of R2
 for N1 being net of R1, N2 being net of R2 st N1 = N2
 for J1 being 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 being 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 15;
       N is NetStr over R2 by A1;
    hence i is net of R2;
   end;
 hence J1 is net_set of the carrier of N2,R2 by YELLOW_6:def 15;
end;

Lm19:
 for R1,R2 being 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 21;
     for e being set st e in Scott-Convergence R1
    holds e in Scott-Convergence R2
   proof let e be set;
    assume
A3:  e in Scott-Convergence R1;
     then consider N1 being Element of NetUniv R1,
                   p1 being Element of R1 such that
A4:   e = [N1,p1] by A2,DOMAIN_1:9;
A5:   N1 in NetUniv R1;
     consider N being strict net of R1 such that
A6:   N1 = N and the carrier of N in the_universe_of the carrier of R1
        by YELLOW_6:def 14;
     reconsider N2 = N1 as strict net of R2 by A1,A6,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 by Def7;
     then p2 <= lim_inf N2 by A1,A8,Lm1;
     then p2 is_S-limit_of N2 by Def7;
    hence e in Scott-Convergence R2 by A4,A7,Def8;
   end;
  hence Scott-Convergence R1 c= Scott-Convergence R2 by TARSKI:def 3;
 end;

Lm20:
 for R1,R2 being complete LATTICE
  st the RelStr of R1 = the RelStr of R2
 holds Scott-Convergence R1 = Scott-Convergence R2
 proof let R1,R2 be complete LATTICE; assume
A1: the RelStr of R1 = the RelStr of R2;
then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19;
     Scott-Convergence R2 c= Scott-Convergence R1 by A1,Lm19;
  hence thesis by A2,XBOOLE_0:def 10;
 end;

Lm21:
 for R1,R2 being 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 is Subset of R1:
   for p being Element of R1 st p in V
    for N being net of R1 st [N,p] in Scott-Convergence R1
      holds N is_eventually_in V} by YELLOW_6:def 27;
A3: the topology of T2 = { V where V is Subset of R2:
 for p being Element of R2 st p in V
    for N being net of R2 st [N,p] in Scott-Convergence R2
      holds N is_eventually_in V} by YELLOW_6:def 27;
   the topology of T1 = the topology of T2
     proof
      thus the topology of T1 c= the topology of T2
       proof let e be set;
        assume e in the topology of T1;
         then consider V1 being Subset of R1 such that
A4:       e = V1 and
A5:       for p being Element of R1 st p in V1
           for N being 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 being Element of R2 st p in V2
           for N being 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;
           then N1 is_eventually_in V1 by A5,A6;
          hence N2 is_eventually_in V2 by A1,Lm6;
         end;
        hence e in the topology of T2 by A3,A4;
       end;
      let e be set;
        assume e in the topology of T2;
         then consider V1 being Subset of R2 such that
A7:       e = V1 and
A8:       for p being Element of R2 st p in V1
           for N being 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 being Element of R1 st p in V2
           for N being 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;
           then N1 is_eventually_in V1 by A8,A9;
          hence N2 is_eventually_in V2 by A1,Lm6;
         end;
        hence e in the topology of T1 by A2,A7;
     end;
  hence sigma R1 = the topology of T2 by Def12
    .= sigma R2 by Def12;

 end;

Lm22:
 for R1,R2 being 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 being Element of R1 such that
A3: X is_<=_than a1 and
A4: for b being Element of R1 st X is_<=_than b holds a1 <= b
      by A2,LATTICE3:def 12;
   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;
   then a1 <= b1 by A4;
  hence a2 <= b2 by A1,Lm1;
 end;

Lm23:
 for R1,R2 being 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 R1 is continuous;
then A2: R1 is satisfying_axiom_of_approximation by WAYBEL_3:def 6;
 thus
A3: for x being Element of R2 holds waybelow x is non empty directed;
  thus R2 is up-complete;
A4: for x being Element of R1 holds waybelow x is non empty directed;
     for x,y being Element of R2 st not x <= y
    ex u being 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
A5:    u1 << x1 and
A6:    not u1 <= y1 by A2,A4,WAYBEL_3:24;
     reconsider u2 = u1 as Element of R2 by A1;
    take u2;
    thus u2 << x2 by A1,A5,Lm15;
    thus not u2 <= y2 by A1,A6,Lm1;
   end;
  hence R2 is satisfying_axiom_of_approximation by A3,WAYBEL_3:24;
 end;

definition let R be continuous complete LATTICE;
  :: 1.6. Proposition (ii)
 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 being Element of R holds waybelow x is non empty directed;
     reconsider p' = p as Element of R;
     consider N being 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 14;
       not p is_S-limit_of N by A1,A2,A4,Def8;
     then not p <= lim_inf X by A4,Def7;
     then consider u being Element of R such that
A5:   u << p' and
A6:   not u <= lim_inf X by A3,WAYBEL_3:24;
      set A = { a where a is Element of R : not a >= u};
        X is_often_in A
       proof let i be Element of X;
         set B = { X.j where j is Element of X: j >= i};
         set C = {"/\"({X.k where k is Element of X:
                    k >= j},R) where j is Element of X:
                   not contradiction};
A7:       lim_inf X = "\/"(C,R) by Def6;
           "/\"(B,R) in C;
         then "/\"(B,R) <= lim_inf X by A7,YELLOW_2:24;
         then not u <= "/\"(B,R) by A6,YELLOW_0:def 2;
         then not u is_<=_than B by YELLOW_0:33;
         then consider b being Element of R such that
A8:       b in B and
A9:       not u <= b by LATTICE3:def 8;
         consider j being Element of X such that
A10:       b = X.j and
A11:       j >= i by A8;
        take j;
        thus i <= j by A11;
        thus X.j in A by A9,A10;
       end;
      then reconsider Y = X"A as subnet of X by YELLOW_6:31;
     take Y;
      reconsider UN = the_universe_of the carrier of R as universal set;
A12:   ex N being strict net of R st X = N &
          the carrier of N in UN by A1,YELLOW_6:def 14;
        X"A is SubRelStr of X by YELLOW_6:def 8;
      then the carrier of X"A c= the carrier of X by YELLOW_0:def 13;
      then the carrier of Y in UN by A12,CLASSES1:def 1;
     hence Y in NetUniv R by YELLOW_6:def 14;
     let Z be subnet of Y;
     assume
A13:   [Z,p] in C;
        C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 21;
      then A14:    Z in NetUniv R by A13,ZFMISC_1:106;
      then consider ZZ being strict net of R such that
A15:    ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 14;
    deffunc F(Element of Z)
     = "/\"({Z.i where i is Element of Z: i >= $1},R);
    defpred P[set] means not contradiction;
      set D = {F(j) where j is Element of Z: P[j]};
        D is Subset of R from SubsetFD;
      then reconsider D as Subset of R;
      reconsider D as non empty directed Subset of R by Th30;
A16:   lim_inf Z = sup D by Def6;
        p is_S-limit_of ZZ by A13,A14,A15,Def8;
      then p <= lim_inf Z by A15,Def7;
      then consider d being Element of R such that
A17:     d in D and
A18:    u <= d by A5,A16,WAYBEL_3:def 1;
      consider j being Element of Z such that
A19:   d = "/\"({Z.k where k is Element of Z: k >= j},R) by A17;
      reconsider j' = j as Element of Z;
      consider i being Element of Z such that
A20:   i >= j' & i >= j' by YELLOW_6:def 5;
      consider f being map of Z, Y such that
A21:   the mapping of Z = (the mapping of Y)*f and
         for m being Element of Y ex n being Element of Z st
        for p being Element of Z st n <= p holds m <= f.p by YELLOW_6:def 12;
        Z.i in {Z.k where k is Element of Z: k >= j} by A20;
      then A22:    d <= Z.i by A19,YELLOW_2:24;
        Y.(f.i) = (the mapping of Y).(f.i) by WAYBEL_0:def 8
        .= ((the mapping of Y)*f).i by FUNCT_2:21
        .= Z.i by A21,WAYBEL_0:def 8;
      then Z.i in A by Th35;
      then ex a being Element of R st a = Z.i & not a >= u;
     hence contradiction by A18,A22,YELLOW_0:def 2;
    end;
   thus C is (ITERATED_LIMITS)
    proof let X be net of R, p be Element of R such that
A23:  [X,p] in C;
     let J be net_set of the carrier of X, R such that
A24:   for i being Element of X holds [J.i,X.i] in C;
A25:    C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 21;
      then A26:  X in NetUniv R by A23,ZFMISC_1:106;
        for i being Element of X holds J.i in NetUniv R
       proof let i be Element of X;
           [J.i,X.i] in C by A24;
        hence J.i in NetUniv R by A25,ZFMISC_1:106;
       end;
then A27:   Iterated J in NetUniv R by A26,YELLOW_6:34;
      reconsider p' = p as Element of R;
      set q = lim_inf Iterated J;
        q is_>=_than waybelow p'
       proof let u be Element of R;
        assume u in waybelow p';
         then A28:          u << p' by WAYBEL_3:7;
         set T = TopRelStr(#the carrier of R,the InternalRel of R, sigma R#);
A29:       the RelStr of T = the RelStr of R;
        the carrier of R = the carrier of ConvergenceSpace C
               by YELLOW_6:def 27;
then A30:        the TopStruct of T = the TopStruct of ConvergenceSpace C by
Def12;
         then reconsider T as TopLattice by A29,Lm3,Lm9;
         reconsider T as complete TopLattice by A29,Lm22;
         reconsider T as continuous complete TopLattice by A29,Lm23;
           the topology of T = sigma T by A29,Lm21;
         then reconsider T as continuous complete Scott TopLattice
                             by Th37;
         :: we now move all to T setting
         reconsider XX = X as net of T;
         reconsider JJ = J as net_set of the carrier of XX,T by A29,Lm18;
         reconsider uu = u, qq = q, pp = p' as Element of T
           ;
         set N = Iterated JJ;
         set CC = Convergence T;
           CC = Convergence ConvergenceSpace C by A30,Lm8;
then A31:       C c= CC by YELLOW_6:49;
A32:      uu << pp by A28,A29,Lm15;
           N = Iterated J by A29,Lm17;
then A33:     qq = lim_inf N by A29,Lm16;
           for i being Element of XX holds [JJ.i,XX.i] in CC
          proof let i be Element of XX;
            reconsider ii = i as Element of X;
A34:          X.ii = (the mapping of X).ii by WAYBEL_0:def 8
              .= (the mapping of XX).i
              .= XX.i by WAYBEL_0:def 8;
              [J.ii,X.ii] in C by A24;
           hence [JJ.i,XX.i] in CC by A31,A34;
          end;
         then [N,pp] in CC by A23,A31,YELLOW_6:def 26;
then A35:      pp in Lim N by YELLOW_6:def 22;
A36:      wayabove uu is open by Th36;
           pp in wayabove uu by A32,WAYBEL_3:8;
         then wayabove uu is a_neighborhood of pp by A36,CONNSP_2:5;
         then A37:       N is_eventually_in wayabove uu by A35,YELLOW_6:def 18;
           wayabove uu c= uparrow uu by WAYBEL_3:11;
         then N is_eventually_in uparrow uu by A37,WAYBEL_0:8;
         then uu <= qq by A33,Th18;
        hence u <= q by A29,Lm1;
       end;
      then sup waybelow p' <= q by YELLOW_0:32;
      then p <= q by WAYBEL_3:def 5;
      then p is_S-limit_of Iterated J by Def7;
     hence [Iterated J,p] in C by A27,Def8;
    end;
  end;
end;

theorem :: Corrollary to Proposition 1.6 (p.103)
   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:53;
  consider M being 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
14
;
     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 x in Lim N by YELLOW_6:def 22;
  end;
 assume x in Lim N;
  then [M,x] in Scott-Convergence T by A1,A2,A3,A4,YELLOW_6:def 22;
 hence x is_S-limit_of N by A1,A3,Def8;
end;

theorem Th39: :: 1.7. Lemma
 for L being 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 being 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 being Element of I holds rng(F.j) is directed;
    set x = Inf Sups F;
A5: x >= Sup Infs Frege F by WAYBEL_5:16;

    reconsider r = [:I,I:] as Relation of I by RELSET_1:def 1;
      dom F = I by PBOOLE:def 3;
    then reconsider f = Sups F as Function of I, the carrier of L;
    set X = NetStr(#I,r,f#);
A6: for i,j being Element of X holds i <= j
     proof let i,j be Element of X;
         [i,j] in the InternalRel of X by ZFMISC_1:106;
      hence i <= j by ORDERS_1:def 9;
     end;
A7: X is transitive
     proof let x,y,z be Element of X such that x <= y & y <= z;
      thus x <= z by A6;
     end;
      X is directed
     proof let x,y be Element of X;
      take x;
      thus x <= x & y <= x 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 being ManySortedSet of I such that
A8:   for i being Element of I holds J.i = F(i) from LambdaDMS;
      for i being 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 i' = i as Element of I;
       reconsider rFi = rng(F.i') as Subset of L;
A9:     rFi is directed by A4;
         J.i' = Net-Str(K.i',F.i') by A8;
      hence J.i is net of L by A9,Th20;
     end;
    then reconsider J as net_set of the carrier of X, L by YELLOW_6:33;
A10:  for j be set st j in I
     ex R being 1-sorted st R = J.j & K.j = the carrier of R
     proof let i be set;
      assume i in I;
       then reconsider i' = i as Element of I;
      take R = Net-Str(K.i',F.i');
      thus R = J.i by A8;
      thus K.i = the carrier of R by Def10;
     end;
A11:  doms F = K by YELLOW_7:45
       .= Carrier J by A10,PRALG_1:def 13;
A12:  dom Frege F = product doms F by PBOOLE:def 3;
then A13:  dom Infs Frege F = product doms F by FUNCT_2:def 1;
A14: for i being Element of X holds J.i in NetUniv L
     proof let i be Element of X;
       reconsider i' = i as Element of I;
A15:   J.i = Net-Str(K.i',F.i') by A8;
       then reconsider Ji = J.i as strict net of L;
         K.i' 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 J.i in NetUniv L by YELLOW_6:def 14;
     end;
A16: for i being Element of X holds [J.i,X.i] in C
     proof let i be Element of X;
       reconsider i' = i as Element of I;
A17:   J.i = Net-Str(K.i',F.i') 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 A19:    i' in dom F by PBOOLE:def 3;
         X.i = (Sups F).i by WAYBEL_0:def 8
          .= Sup(F.i') by A19,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 by Def7;
      hence [J.i,X.i] in C by A17,A18,Def8;
     end;
A20: X in NetUniv L by A2,YELLOW_6:def 14;
then A21:  Iterated J in NetUniv L by A14,YELLOW_6:34;
    deffunc I(Element of Iterated J) =
     {(Iterated J).p where p is Element of Iterated J :p >= $1};
      the carrier of Iterated J = [:the carrier of X, product Carrier J:]
          by YELLOW_6:35;
    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 is Element of X :i >= $1};
    defpred P[set] means not contradiction;
    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 = {"/\"(I(j),L) where j is Element of Iterated J:
               not contradiction};
    set D' = {F(i,g) where i is Element of X,
                    g is Element of product doms F: P[g]};
    set E' = {F(g) where g is Element of product doms F : P[g]};
A22:  for i being Element of X, g being 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 being set holds y in I(j,g) iff
        ex x being set st x in dom((Frege F).g) & y = ((Frege F).g).x
      proof let y be set;
          g in product Carrier J by A11;
then A23:      g in the carrier of product J by YELLOW_1:def 4;
       hereby assume y in I(j,g);
         then consider i being Element of X such that
A24:       y =G.(i,g) and
            i >= j;
         reconsider x = i as set;
        take x;
         reconsider i' = i as Element of I;
          i in I;
then A25:      i' in dom F by PBOOLE:def 3;
        hence x in dom((Frege F).g) by A12,WAYBEL_5:8;
        thus ((Frege F).g).x
          = F.i'.(g.i) by A12,A25,WAYBEL_5:9
         .= (the mapping of Net-Str(K.i',F.i')).(g.i) by Def10
         .= (the mapping of J.i).(g.i) by A8
         .= y by A23,A24,YELLOW_6:def 16;
       end;
       given x being set 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;
        then reconsider i' = x as Element of I by PBOOLE:def 3;
        reconsider i = i' 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.i',F.i')).(g.i) by Def10
         .= (the mapping of J.i).(g.i) by A8
         .= G.(i,g) by A23,YELLOW_6:def 16;
       hence y in I(j,g) by A29;
      end;
     hence "/\"(rng((Frege F).g),L) = "/\"(I(j,g),L) by FUNCT_1:def 5;
    end;
A30: D = D'
     proof
A31:    the carrier of Iterated J = [:the carrier of X, product Carrier J:]
                                      by YELLOW_6:35;
A32: for p being Element of Iterated J,
          i being Element of X,
          g being 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 16;
           g in product Carrier J by A11;
         then g in the carrier of product J by YELLOW_1:def 4;
         then reconsider g' = g as Element of product J;
           g' in the carrier of product J;
then A35:      g' in product Carrier J by YELLOW_1:def 4;
         reconsider i' = i as Element of X;
           for i be set st i in the carrier of X
          ex R being RelStr, xi,yi being Element of R
            st R = J.i & xi = g'.i & yi = g'.i & xi <= yi
          proof let i be set;
           assume i in the carrier of X;
            then reconsider ii = i as Element of X;
            reconsider i' = ii as Element of I;
A36:      J.i = Net-Str(K.i',F.i') by A8;
             set R = Net-Str(K.i',F.i');
              g'.ii in the carrier of R by A36;
            then reconsider x = g'.i as Element of R;
           take R,x,x;
              x <= x;
          hence thesis by A8;
          end;
then A37:      g' <= g' by A35,YELLOW_1:def 4;

           I(i,g) c= I(p)
          proof let u be set;
           assume u in I(i,g);
            then consider j being Element of X such that
A38:          u = (the mapping of Iterated J).(j,g) and
A39:          j >= i;
            reconsider j' = j as Element of X;
            reconsider q = [j,g] as Element of Iterated J
               by A11,A31,ZFMISC_1:106;
              [j',g'] >= [i',g'] by A37,A39,YELLOW_3:11;
then A40:          q >= p by A33,A34,Lm1;
              u = (the mapping of Iterated J). [j,g] by A38,BINOP_1:def 1
             .= (Iterated J).q by WAYBEL_0:def 8;
           hence u in I(p) by A40;
          end;
then A41:       "/\"(I(p),L) <= "/\"(I(i,g),L) by WAYBEL_7:3;
         defpred P[Element of X] means $1 >= i;
         deffunc F(Element of X) = G.($1,g);
          {F(k) where k is Element of X: P[k]}
           is Subset of L from SubsetFD;
         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 is Element of Iterated J: P[z]}
             is Subset of L from SubsetFD;
         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 being Element of Iterated J
            such that
A42:          b = (Iterated J).q and
A43:          p <= q;
            consider k being Element of X,
                     f being Element of product Carrier J such that
A44:          q = [k,f] by A31,DOMAIN_1:9;
            reconsider k' = 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;
              f in product Carrier J;
            then f in the carrier of product J by YELLOW_1:def 4;
            then reconsider f' = f as Element of product J;
A45:         [k',f'] >= [i',g'] by A33,A34,A43,A44,Lm1;
            then i <= k by YELLOW_3:11;
           hence a in A;
            reconsider k' = k as Element of I;
            set N = Net-Str(K.k',F.k');

A46:      J.k = N by A8;
            reconsider g'k =g'.k, f'k = f'.k as Element of N
                  by A8;
A47:          b = (the mapping of J.k).(f'.k) by A42,A44,YELLOW_6:36
             .= N.(f'k) by A46,WAYBEL_0:def 8;
            reconsider kg = [k,g] as Element of Iterated J
               by A11,A31,ZFMISC_1:106;
A48:          a = (the mapping of Iterated J).kg by BINOP_1:def 1
             .= (Iterated J).kg by WAYBEL_0:def 8
             .= (the mapping of J.k).(g'.k) by YELLOW_6:36
             .= N.(g'k) by A46,WAYBEL_0:def 8;
              g' <= f' by A45,YELLOW_3:11;
            then g'.k <= f'.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 "/\"(I(p),L) = "/\"(I(i,g),L) by A41,YELLOW_0:def 3;
       end;
      thus D c= D'
       proof let e be set;
        assume e in D;
         then consider p being Element of Iterated J such that
A49:        e = "/\"(I(p),L);
         consider j being Element of X,
                  g being Element of product doms F such that
A50:      p = [j,g] by A11,A31,DOMAIN_1:9;
           e = "/\"(I(j,g),L) by A32,A49,A50;

        hence e in D';
       end;
      let e be set;
      assume e in D';
       then consider i being Element of X,
                     g being Element of product doms F such that
A51:     e = "/\"(I(i,g),L);
       reconsider j = [i,g] as Element of Iterated J
                    by A11,A31,ZFMISC_1:106;
         e = "/\"(I(j),L) by A32,A51;
      hence e in D;
     end;
A52: E' = D' from Irrel(A22); :: UWAGA!!! wrazliwy na strony rownosci
      for y being set holds y in E' iff
        ex x being set st x in dom(Infs Frege F) & y = (Infs Frege F).x
     proof let y be set;
      thus y in E' implies
        ex x being set st x in dom(Infs Frege F) & y = (Infs Frege F).x
      proof assume y in E';
       then consider g being Element of product doms F such that
A53:      y = "/\"(rng((Frege F).g),L);
       take g;
       thus g in dom(Infs Frege F) by A13;
then A54:      g in dom(Frege F) by FUNCT_2:def 1;
       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 being set 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 A12,A55,FUNCT_2:def 1;
         x in dom(Frege F) by A55,FUNCT_2:def 1;
       then y = //\((Frege F).x, L) by A56,WAYBEL_5:def 2
        .= "/\"(rng((Frege F).x),L) by YELLOW_2:def 6;
      hence y in E';
     end;
    then rng Infs Frege F = E' by FUNCT_1:def 5;
then A57:  Sup Infs Frege F = "\/"(D,L) by A30,A52,YELLOW_2:def 5
        .= lim_inf Iterated J by Def6;
    reconsider x' = x as Element of L;
    set X1 = {x where j' is Element of X: not contradiction},
        X2 = {"/\"({X.i where i is Element of X:i >= j},L)
           where j is Element of X: not contradiction};
A58:  X2 = X1
     proof
A59:    for j being Element of X holds
        x = "/\"({X.i where i is Element of X:i >= j},L)
      proof let j be Element of X;
        set X3 = {X.i where i is Element of X:i >= j};
          for e being set holds e in X3 iff
           ex u being set st u in dom Sups F & e = (Sups F).u
        proof let e be set;
         hereby assume e in X3;
           then consider i being Element of X such that
A60:         e = X.i and
              i >= j;
           reconsider u = i as set;
          take u;
             u in I;
          hence u in dom Sups F by FUNCT_2:def 1;
          thus e = (Sups F).u by A60,WAYBEL_0:def 8;
         end;
         given u being set 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,WAYBEL_0:def 8;
         hence e in X3 by A63;
        end;
        then rng Sups F = X3 by FUNCT_1:def 5;
       hence x = "/\"(X3,L) by YELLOW_2:def 6;
      end;
      thus X2 c= X1
       proof let u be set;
        assume u in X2;
         then consider j being Element of X such that
A64:        u = "/\"({X.i where i is Element of X:i >= j},L);
           u = x by A59,A64;
        hence u in X1;
       end;
      let u be set;
       consider j being Element of X;
      assume u in X1;
       then ex j being Element of X st u = x;
       then u = "/\"({X.i where i is Element of X:i >=
 j},L) by A59
;
      hence u in X2;
     end;
  now let u be set;
        u in X1 iff ex j' being 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 {x'} by A58,TARSKI:2
    .= x by YELLOW_0:39;
    then x <= lim_inf X by Def6;
    then x is_S-limit_of X by Def7;
    then [X,x] in C by A20,Def8;

    then [Iterated J,x] in C by A1,A16,YELLOW_6:def 26;
    then x is_S-limit_of Iterated J by A21,Def8;
    then x <= Sup Infs Frege F by A57,Def7;
   hence x = Sup Infs Frege F by A5,ORDERS_1:25;
  end;
 hence L is continuous by WAYBEL_5:18;
end;

theorem :: 1.8 Theorem, p.104
   for T being 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:53;
 end;
 thus thesis by Th39;
end;

theorem Th41: :: 1.9 Remark, p.104
 for T being complete Scott TopLattice,
     S being 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 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 being Element of T such that
A2:   y in S and
A3:   y << sup D by A1;
     consider d being Element of T such that
A4:   d in D and
A5:   y <= d by A3,WAYBEL_3:def 1;
        d in S by A2,A5,WAYBEL_0:def 20;
    hence D meets S by A4,XBOOLE_0:3;
   end;
 hence S is open by Def4;
end;

theorem Th42:
 for L being non empty RelStr, S being upper Subset of L,
     x being 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 set;
 assume
A2: e in uparrow x;
  then reconsider y = e as Element of L;
    x <= y by A2,WAYBEL_0:18;
 hence e in S by A1,WAYBEL_0:def 20;
end;

theorem Th43:
 for L being complete continuous Scott TopLattice,
     p be Element of L, S be Subset of L st S is open & p in S
  ex q being 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,Def1;
    then (waybelow p) /\ S <> {} by XBOOLE_0:def 7;
    then consider u being Element of L such that
A4:   u in (waybelow p) /\ S by SUBSET_1:10;
     reconsider u as Element of L;
    take u;
       u in waybelow p by A4,XBOOLE_0:def 3;
    hence u << p by WAYBEL_3:7;
    thus u in S by A4,XBOOLE_0:def 3;
end;

theorem Th44: :: 1.10. Propostion (i), p.104
 for L being complete continuous Scott TopLattice,
     p be Element of L
  holds { wayabove q where q is 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 is Element of L: q << p };
    X c= bool the carrier of L
   proof let e be set;
    assume e in X;
     then ex q being Element of L st e = wayabove q & q << p;
    hence e in bool the carrier of L;
   end;
  then X is Subset-Family of L by SETFAM_1:def 7;
  then reconsider X as Subset-Family of L;
    X is Basis of p
   proof
    thus X c= the topology of L
     proof let e be set;
      assume e in X;
       then consider q being Element of L such that
A1:     e = wayabove q and q << p;
         wayabove q is open by Th36;
      hence e in the topology of L by A1,PRE_TOPC:def 5;
     end;
       for Y being set st Y in X holds p in Y
      proof let e be set;
       assume e in X;
        then ex q being Element of L st e = wayabove q & q << p;
       hence p in e by WAYBEL_3:8;
      end;
    hence p in Intersect X by CANTOR_1:10;
    let S be Subset of L such that
A2:  S is open and
A3:  p in S;
     consider u being Element of L such that
A4:  u << p and
A5:  u in S by A2,A3,Th43;
    take V = wayabove u;
    thus V in X by A4;
A6:   S is upper by A2,Def4;
A7:   wayabove u c= uparrow u by WAYBEL_3:11;
       uparrow u c= S by A5,A6,Th42;
    hence V c= S by A7,XBOOLE_1:1;
   end;
 hence thesis;
end;

theorem Th45:
 for T being complete continuous Scott TopLattice holds
 { wayabove x where x is Element of T: not contradiction } is Basis of T
proof let T be complete continuous Scott TopLattice;
 set B = { wayabove x where x is Element of T: not contradiction };
A1: B c= the topology of T
  proof let e be set;
   assume e in B;
    then consider x being Element of T such that
A2:  e = wayabove x;
      wayabove x is open by Th36;
   hence e in the topology of T by A2,PRE_TOPC:def 5;
  end;
 then B c= bool the carrier of T by XBOOLE_1:1;
 then B is Subset-Family of T by SETFAM_1:def 7;
 then reconsider P = B as Subset-Family of T;
    for x being Point of T ex B being 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 is Element of T: q << p } as Basis of x
           by Th44;
    take A;
    let u be set;
    assume u in A;
     then ex q being Element of T st u = wayabove q & q << p;
    hence u in P;
   end;
 hence B is Basis of T by A1,YELLOW_8:23;
end;

theorem  :: 1.10. Propostion (ii), p.104
   for T being complete continuous Scott TopLattice,
     S being 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  :: 1.10. Propostion (iii), p.104
   for T being complete continuous Scott TopLattice,
     p being 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 set;
   assume
A1:  y in Int uparrow p;
    then reconsider q = y as Element of T;
    reconsider S = Int uparrow p as Subset of T;
      S is open by TOPS_1:51;
    then consider u being Element of T such that
A2:  u << q and
A3:  u in S by A1,Th43;
      S c= uparrow p by TOPS_1:44;
    then p <= u by A3,WAYBEL_0:18;
    then p << q by A2,WAYBEL_3:2;
   hence y in wayabove p by WAYBEL_3:8;
  end;
A4: wayabove p is open by Th36;
    wayabove p c= uparrow p by WAYBEL_3:11;
 hence wayabove p c= Int uparrow p by A4,TOPS_1:56;
end;

theorem  :: 1.10. Propostion (iv), p.104
   for T being complete continuous Scott TopLattice,
     S being Subset of T
  holds Int S = union{wayabove x where x is Element of T: wayabove x c= S}
proof
 let T be complete continuous Scott TopLattice,
     S be Subset of T;
  set B = { wayabove x where x is Element of T: not contradiction },
      I = { G where G is Subset of T: G in B & G c= S },
      P = {wayabove x where x is Element of T: wayabove x c= S};
A1: I = P
   proof
    thus I c= P
     proof let e be set;
      assume e in I;
       then consider G being Subset of T such that
A2:     e = G and
A3:     G in B and
A4:     G c= S;
         ex x being Element of T st G = wayabove x by A3;
      hence e in P by A2,A4;
     end;
    let e be set;
    assume e in P;
     then consider x being Element of T such that
A5:  e = wayabove x and
A6:  wayabove x c= S;
       wayabove x in B;
    hence e in I by A5,A6;
   end;
    B is Basis of T by Th45;
 hence Int S = union P by A1,YELLOW_8:20;
end;

Back to top