:: Scott Topology
::  by Andrzej Trybulec
::
:: Received January 29, 1997
:: Copyright (c) 1997-2016 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ORDERS_2, SUBSET_1, XXREAL_0, XBOOLE_0, TARSKI, REWRITE1,
      WAYBEL_0, SETFAM_1, LATTICES, LATTICE3, EQREL_1, RELAT_2, FINSET_1,
      ORDINAL2, YELLOW_0, ZFMISC_1, STRUCT_0, CARD_1, RELAT_1, CARD_FIL,
      WAYBEL_9, RCOMP_1, NATTRA_1, PRE_TOPC, T_0TOPSP, CONNSP_2, TOPS_1,
      FUNCT_1, YELLOW_6, SEQM_3, CLASSES2, CLASSES1, YELLOW_2, PROB_1,
      WAYBEL_3, ORDINAL1, CARD_3, PBOOLE, WAYBEL_5, FUNCT_6, RLVECT_2,
      WAYBEL_6, RLVECT_3, YELLOW_8, WAYBEL11;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, RELAT_1, SETFAM_1,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, FUNCT_6, DOMAIN_1,
      ORDINAL1, NUMBERS, STRUCT_0, WAYBEL_6, PRE_TOPC, TOPS_1, TOPS_2,
      CANTOR_1, CONNSP_2, T_0TOPSP, TDLAT_3, PBOOLE, CLASSES1, CLASSES2,
      CARD_3, PRALG_1, ORDERS_2, 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 DOMAIN_1, CLASSES1, CLASSES2, TOPS_1, CONNSP_2, TDLAT_3,
      T_0TOPSP, CANTOR_1, PRALG_1, PRALG_2, ORDERS_3, WAYBEL_1, YELLOW_4,
      WAYBEL_3, WAYBEL_5, WAYBEL_6, WAYBEL_9, YELLOW_8, RELSET_1, TOPS_2,
      WAYBEL_2, NUMBERS;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1,
      CARD_3, CLASSES2, PBOOLE, STRUCT_0, LATTICE3, YELLOW_0, TDLAT_3,
      WAYBEL_0, YELLOW_1, WAYBEL_3, YELLOW_6, WAYBEL_5, WAYBEL_9, RELSET_1,
      TOPS_1;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions STRUCT_0, XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3,
      YELLOW_0, RELAT_1, YELLOW_6, YELLOW_4, WAYBEL_1, WAYBEL_3, TOPS_2,
      YELLOW_8, WAYBEL_6;
 equalities STRUCT_0, SUBSET_1, WAYBEL_0, YELLOW_6, WAYBEL_3, BINOP_1;
 expansions XBOOLE_0, TARSKI, PRE_TOPC, WAYBEL_0, LATTICE3, YELLOW_0, YELLOW_6,
      YELLOW_4, WAYBEL_1, WAYBEL_3;
 theorems TSP_1, WAYBEL_0, YELLOW_0, TARSKI, SUBSET_1, TOPS_1, YELLOW_2,
      SETFAM_1, CONNSP_2, ZFMISC_1, RELSET_1, TDLAT_3, TEX_1, ORDERS_2,
      LATTICE3, YELLOW_6, WAYBEL_5, DOMAIN_1, WAYBEL_7, YELLOW_1, YELLOW_3,
      WAYBEL_3, FUNCT_1, FUNCT_2, YELLOW_7, PRALG_1, WAYBEL_2, CLASSES1,
      RELAT_1, WAYBEL_4, YELLOW_8, XBOOLE_0, XBOOLE_1, PARTFUN1;
 schemes RELSET_1, DOMAIN_1, FRAENKEL, PBOOLE, XFAMILY;

begin :: Preliminaries

Lm1: for R,S being RelStr, p,q being Element of R, p9,q9 being Element of S
st p = p9 & q = q9 & the RelStr of R = the RelStr of S
holds p <= q implies p9 <= q9
proof
  let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that
A1: p = p9 and
A2: q = q9 and
A3: the RelStr of R = the RelStr of S;
  assume p <= q;
  then [p9,q9] in the InternalRel of S by A1,A2,A3,ORDERS_2:def 5;
  hence thesis by ORDERS_2:def 5;
end;

scheme 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 object;
    set i = the Element of I();
    assume e in A;
    then consider u being Element of D() such that
A2: e = F(u) and
A3: P[u];
    e = F(i,u) by A1,A2;
    hence thesis by A3;
  end;
  let e be object;
  assume e in B;
  then consider i being Element of I(), u being Element of D() such that
A4: e = F(i,u) and
A5: P[u];
  e = F(u) by A1,A4;
  hence thesis by A5;
end;

theorem 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;
    "/\"(X,L) <= x by A2,YELLOW_2:22;
    hence "/\"(X,L) <= y by A3,YELLOW_0:def 2;
  end;
  hence thesis by YELLOW_0:33;
end;

theorem 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;
    "\/"(Y,L) >= y by A2,YELLOW_2:22;
    hence thesis by A3,YELLOW_0:def 2;
  end;
  hence thesis by YELLOW_0:32;
end;

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

registration
  let T be reflexive non empty RelStr;
  cluster non empty directed finite for Subset of T;
  existence
  proof set x = the Element of T;
    take {x};
    thus thesis by WAYBEL_0:5;
  end;
end;

theorem 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;
  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;
A6: x >= c by A2,A5;
    c >= x by A1,A4;
    hence thesis by A6,ORDERS_2:2;
  end;
  then ex_sup_of D,T by A2,A3;
  hence thesis by A1,A2,A3,YELLOW_0:def 9;
end;

registration
  cluster reflexive transitive 1-element antisymmetric
    with_suprema with_infima finite strict for RelStr;
  existence
  proof
    0 in {0} by TARSKI:def 1;
    then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
    reconsider T = RelStr(#{0},r#) as non empty RelStr;
    take T;
    thus T is reflexive
    proof
      let x be Element of T;
      x = 0 by TARSKI:def 1;
      then [x,x] in {[0,0]} by TARSKI:def 1;
      hence thesis by ORDERS_2:def 5;
    end;
    then reconsider T9 = T as 1-element reflexive RelStr;
    T9 is transitive;
    hence T is transitive;
    thus T is 1-element;
    T9 is antisymmetric;
    hence T is antisymmetric;
    T9 is with_suprema;
    hence T is with_suprema;
    T9 is with_infima;
    hence T is with_infima;
    thus T is finite;
    thus thesis;
  end;
end;

registration
  let T be finite 1-sorted;
  cluster -> finite for Subset of T;
  coherence;
end;

registration
  let R be RelStr;
  cluster empty -> lower upper for Subset of R;
  coherence;
end;

registration
  let R be 1-element RelStr;
  cluster -> upper for Subset of R;
  coherence
  proof
    let S be Subset of R;
    ex x being Element of R st ( the carrier of R = {x}) by TEX_1:def 1;
    then S = {}R or S = [#]R by ZFMISC_1:33;
    hence thesis;
  end;
end;

theorem 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 object such that
A2: y in A and
A3: y in downarrow x by XBOOLE_0:3;
  reconsider y as Element of T by A2;
  y <= x by A3,WAYBEL_0:17;
  hence contradiction by A1,A2,WAYBEL_0:def 20;
end;

theorem 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 XBOOLE_0:def 5;
  then A` misses downarrow x by Th5;
  then A` c= (downarrow x)` by SUBSET_1:23;
  hence thesis by SUBSET_1:12;
end;

begin :: 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;
  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;
  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;
end;

notation
  let T be non empty reflexive RelStr, S be Subset of T;
  synonym S is inaccessible for S is inaccessible_by_directed_joins; synonym
  S is directly_closed for S is closed_under_directed_sups;
end;

registration
  let T be non empty reflexive RelStr;
  cluster empty -> property(S) directly_closed for Subset of T;
  coherence;
end;

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

registration
  let T be non empty reflexive RelStr, S be property(S) Subset of T;
  cluster S` -> directly_closed;
  coherence
  proof
    let D be non empty directed Subset of T such that
A1: D c= S`;
    assume not sup D in S`;
    then sup D in S by XBOOLE_0:def 5;
    then consider y 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 4;
    then D meets S;
    hence contradiction by A1,SUBSET_1:23;
  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;

registration
  let T be reflexive transitive antisymmetric non empty with_suprema
  finite RelStr;
  cluster -> inaccessible for Subset of T;
  coherence
  proof
    let S be Subset of T, D be non empty directed Subset of T such that
A1: sup D in S;
    sup D in D by Th4;
    hence thesis by A1,XBOOLE_0:3;
  end;
end;

definition
  let T be reflexive transitive antisymmetric non empty with_suprema
  finite TopRelStr;
  redefine attr T is Scott means
  for S being Subset of T holds S is open iff S is upper;
  compatibility;
end;

registration
  cluster complete strict 1-element Scott for TopLattice;
  existence
  proof
set T = the reflexive 1-element discrete strict finite TopRelStr;
    take T;
    thus T is complete strict 1-element;
    let S be Subset of T;
    thus thesis by TDLAT_3:15;
  end;
end;

registration
  let T be non empty reflexive RelStr;
  cluster [#]T -> directly_closed inaccessible;
  coherence
  proof
    thus [#]T is directly_closed;
    let D be non empty directed Subset of T such that sup D in [#]T;
    ex p being Element of T st ( p in D) by SUBSET_1:4;
    hence D meets [#]T by XBOOLE_0:3;
  end;
end;

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

registration
  let T be non empty reflexive RelStr, S be inaccessible Subset of T;
  cluster S` -> directly_closed;
  coherence
  proof
    let D be non empty directed Subset of T;
    assume D c= S`;
    then D misses S by SUBSET_1:23;
    then not sup D in S by Def1;
    hence thesis by XBOOLE_0:def 5;
  end;
end;

registration
  let T be non empty reflexive RelStr, S be directly_closed Subset of T;
  cluster S` -> inaccessible;
  coherence
  proof
    let D be non empty directed Subset of T;
    assume sup D in S`;
    then not sup D in S by XBOOLE_0:def 5;
    then not D c= S`` by Def2;
    hence thesis by SUBSET_1:23;
  end;
end;

theorem 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;
    then reconsider A = S` as inaccessible upper Subset of T by Def4;
    A` is directly_closed lower;
    hence S is directly_closed lower;
  end;
  assume S is directly_closed lower;
  then reconsider S as directly_closed lower Subset of T;
  S` is open by Def4;
  hence thesis;
end;

theorem 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
    by A1,WAYBEL_0:17;
    then sup D <= x by A2,YELLOW_0:30;
    hence thesis by WAYBEL_0:17;
  end;
  hence thesis;
end;

theorem 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:31;
  now
    let C be Subset of T such that
A3: {x} c= C;
    reconsider D = C as Subset of T;
    assume C is closed;
    then
A4: D is lower by Th7;
    x in C by A3,ZFMISC_1:31;
    hence downarrow x c= C by A4,Th6;
  end;
  hence thesis by A1,A2,YELLOW_8:8;
end;

theorem  :: 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 x9 = x, y9 = y as Element of T;
A1: Cl {x9} = downarrow x9 by Th9;
A2: Cl {y9} = downarrow y9 by Th9;
    assume x <> y;
    hence Cl {x} <> Cl {y} by A1,A2,WAYBEL_0:19;
  end;
  hence thesis by TSP_1:def 5;
end;

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

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 thesis;
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:23;
  A misses downarrow x by A1,Th5;
  then A c= (downarrow x)` by SUBSET_1:23;
  hence thesis by A2,CONNSP_2:def 2;
end;

theorem  :: 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-Family of T from DOMAIN_1:sch 7;
  then reconsider F as Subset-Family of T;
  take F;
  thus S = meet F
  proof
    [#]T is a_neighborhood of S by CONNSP_2:28;
    then
A1: [#]T in F;
    now
      let Z1 be set;
      assume Z1 in F;
      then ex X being Subset of T st Z1 = X & X is a_neighborhood of S;
      hence S c= Z1 by CONNSP_2:29;
    end;
    hence S c= meet F by A1,SETFAM_1:5;
    let x be object such that
A2: x in meet F and
A3: not x in S;
    reconsider p = x as Element of T by A2;
    (downarrow p)` is a_neighborhood of S by A3,Th13;
    then (downarrow p)` in F;
    then
A4: meet F c= (downarrow p)` by SETFAM_1:3;
    p <= p;
    then p in downarrow p by WAYBEL_0:17;
    hence contradiction by A2,A4,XBOOLE_0:def 5;
  end;
  let X be Subset of T;
  assume X in F;
  then ex Y being Subset of T st X = Y & Y is a_neighborhood of S;
  hence thesis;
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 is property(S)
    proof
      let D be non empty directed Subset of T such that
A3:   sup D in S;
      S is inaccessible by A1,Def4;
      then S meets D by A3;
      then consider y being object such that
A4:   y in S and
A5:   y in D by XBOOLE_0:3;
      reconsider y as Element of T by A4;
      take y;
      thus thesis by A2,A4,A5;
    end;
  end;
  assume that
A6: S is upper and
A7: S is property(S);
  S is inaccessible
  proof
    let D be non empty directed Subset of T;
    assume sup D in S;
    then consider y 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;
    y >= y by YELLOW_0:def 1;
    then y in S by A8,A9;
    hence thesis by A8,XBOOLE_0:3;
  end;
  hence thesis by A6,Def4;
end;

registration
  let T be complete TopLattice;

:: p. 100, Remark 1.4 (vi)
  cluster lower -> property(S) for Subset of T;
  coherence
  proof
    let S be Subset of T;
    assume
A1: S is lower;
    let D be non empty directed Subset of T such that
A2: sup D in S;
    consider y being Element of T such that
A3: y in D by SUBSET_1:4;
    take y;
    thus y in D by A3;
    let x be Element of T such that
A4: x in D and x >= y;
    x <= sup D by A4,YELLOW_2:22;
    hence thesis by A1,A2;
  end;
end;

Lm2: for T being non empty reflexive TopRelStr holds [#]T is property(S)
proof
  let T be non empty reflexive TopRelStr;
  let D be non empty directed Subset of T such that sup D in [#]T;
  consider y being Element of T such that
A1: y in D by SUBSET_1:4;
  take y;
  thus y in D by A1;
  let x be Element of T such that x in D and x >= y;
  thus thesis;
end;

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

begin :: 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
  "\/"((the set of all "/\"({N.i:i >= j},R) where j is Element of N),R);
  correctness;
end;

definition
  let R be reflexive non empty RelStr;
  let N be net of R, p be Element of R;
  pred p is_S-limit_of N means
  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 RELSET_1:sch 2;
    reconsider C as Convergence-Class of R by YELLOW_6:def 18;
    take C;
    let N be strict net of R such that
A2: N in NetUniv R;
    let p be Element of R;
    hereby
      assume [N,p] in C;
      then ex M 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 thesis 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 object;
A5: it1 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18;
A6: it2 c= [:NetUniv R, the carrier of R:] by YELLOW_6:def 18;
    hereby
      assume
A7:   [x,y] in it1;
      then
A8:   x in NetUniv R by A5,ZFMISC_1:87;
      then consider N 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 11;
      reconsider p = y as Element of R by A5,A7,ZFMISC_1:87;
      p is_S-limit_of N by A3,A7,A8,A9;
      hence [x,y] in it2 by A4,A8,A9;
    end;
    assume
A10: [x,y] in it2;
    then
A11: x in NetUniv R by A6,ZFMISC_1:87;
    then consider N 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 11;
    reconsider p = y as Element of R by A6,A10,ZFMISC_1:87;
    p is_S-limit_of N by A4,A10,A11,A12;
    hence thesis by A3,A11,A12;
  end;
end;

:: 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;
  set X = the set of all "/\"({N.i where i is Element of N:
  i >= j},R) where j is Element of N;
  reconsider q9= q as Element of R;
  q9 is_>=_than X
  proof
    let x be Element of R;
    assume x in X;
    then consider j1 being Element of N such that
A4: 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
A5: j2 >= j0 and
A6: j2 >= j1 by YELLOW_6:def 3;
    N.j2 in Y by A6;
    then
A7: x <= N.j2 by A4,YELLOW_2:22;
    N.j2 in downarrow q by A3,A5;
    then N.j2 <= q9 by WAYBEL_0:17;
    hence x <= q9 by A7,YELLOW_0:def 2;
  end;
  then lim_inf N <= q9 by YELLOW_0:32;
  hence thesis by A1,YELLOW_0:def 2;
end;

theorem 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;
  set X = the set of all "/\"({N.i where i is Element of N:
  i >= j},R) where j is Element of N;
  set Y = {N.i where i is Element of N: i >= j0};
  reconsider q9= q as Element of R;
  "/\"(Y,R) in X;
  then
A2: lim_inf N >= "/\"(Y,R) by YELLOW_2:22;
  q9 is_<=_than Y
  proof
    let y be Element of R;
    assume y in Y;
    then consider i1 being Element of N such that
A3: y = N.i1 and
A4: i1 >= j0;
    reconsider i19 = i1 as Element of N;
    N.i19 in uparrow q by A1,A4;
    hence q9 <= y by A3,WAYBEL_0:18;
  end;
  then "/\"(Y,R) >= q9 by YELLOW_0:33;
  hence thesis by A2,YELLOW_0:def 2;
end;

definition
  let R be reflexive non empty RelStr, N be non empty NetStr over R;
  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;
      let i,j be Element of N;
      assume i <= j;
      hence N.i <= N.j by A1;
    end;
    assume
A2: 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;
A3:   netmap(N,R).x = N.x;
A4:   netmap(N,R).y = N.y;
      assume x <= y;
      hence netmap(N,R).x <= netmap(N,R).y by A2,A3,A4;
    end;
    hence thesis;
  end;
end;

definition
  let R be non empty RelStr;
  let S be non empty set, f be Function of S, the carrier of R;
  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 RELSET_1:sch 2;
    take N = NetStr(#S,R,f#);
    thus the carrier of N = S;
    thus the mapping of N = f;
    let i,j be Element of N;
    reconsider x = i, y = j as Element of S;
    [x,y] in the InternalRel of N iff f.x <= f.y by A1;
    hence thesis by ORDERS_2:def 5;
  end;
  uniqueness
  proof
    let it1,it2 be strict non empty NetStr over R such that
A2: the carrier of it1 = S and
A3: the mapping of it1 = f and
A4: for i,j being Element of it1 holds i <= j iff it1.i <= it1.j and
A5: the carrier of it2 = S and
A6: the mapping of it2 = f and
A7: for i,j 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 object;
      hereby
        assume
A8:     [x,y] in the InternalRel of it1;
        then reconsider i=x, j=y as Element of it1 by ZFMISC_1:87;
        reconsider i9=x, j9=y as Element of it2 by A2,A5,A8,ZFMISC_1:87;
A9:     it1.i = it2.i9 by A3,A6;
A10:    it1.j = it2.j9 by A3,A6;
        i <= j by A8,ORDERS_2:def 5;
        then it2.i9 <= it2.j9 by A4,A9,A10;
        then i9 <= j9 by A7;
        hence [x,y] in the InternalRel of it2 by ORDERS_2:def 5;
      end;
      assume
A11:  [x,y] in the InternalRel of it2;
      then reconsider i=x, j=y as Element of it2 by ZFMISC_1:87;
      reconsider i9=x, j9=y as Element of it1 by A2,A5,A11,ZFMISC_1:87;
A12:  it2.i = it1.i9 by A3,A6;
A13:  it2.j = it1.j9 by A3,A6;
      i <= j by A11,ORDERS_2:def 5;
      then it1.i9 <= it1.j9 by A7,A12,A13;
      then i9 <= j9 by A4;
      hence thesis by ORDERS_2:def 5;
    end;
    hence thesis by A2,A3,A5,A6;
  end;
end;

theorem Th19:
  for L being non empty 1-sorted, N being non empty NetStr over L
  holds rng the mapping of N =
  the set of all  N.i where i is Element of N
proof
  let L be non empty 1-sorted, N be non empty NetStr over L;
  set X = the set of all  N.i where i is Element of N;
A1: the carrier of N = dom the mapping of N by FUNCT_2:def 1;
  thus rng the mapping of N c=
  the set of all  N.i where i is Element of N
  proof
    let e be object;
    assume e in rng the mapping of N;
    then consider u being object such that
A2: u in dom the mapping of N and
A3: e = (the mapping of N).u by FUNCT_1:def 3;
    reconsider u as Element of N by A2;
    e = N.u by A3;
    hence thesis;
  end;
  let e be object;
  assume e in X;
  then ex i being Element of N st ( e = N.i);
  hence thesis by A1,FUNCT_1:def 3;
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;
  f = the mapping of N by Def10;
  then
A2: rng f = the set of all  N.i where i is Element of N by Th19;
  then
A3: N.x in rng f;
  N.y in rng f by A2;
  then consider p being Element of R such that
A4: p in rng f and
A5: N.x <= p and
A6: N.y <= p by A1,A3;
  consider z being object such that
A7: z in dom f and
A8: p = f.z by A4,FUNCT_1:def 3;
  reconsider z as Element of N by A7,Def10;
  take z;
  p = N.z by A8,Def10;
  hence thesis by A5,A6,Def10;
end;

registration
  let R be non empty RelStr;
  let S be non empty set, f be Function of S, the carrier of R;
  cluster Net-Str(S,f) -> monotone;
  coherence
  proof
    set N = Net-Str(S,f);
    netmap(N,R) is monotone
    proof
      let x,y be Element of N;
A1:   netmap(N,R).x = N.x;
A2:   netmap(N,R).y = N.y;
      assume x <= y;
      hence netmap(N,R).x <= netmap(N,R).y by A1,A2,Def10;
    end;
    hence thesis;
  end;
end;

registration
  let R be transitive non empty RelStr;
  let S be non empty set, f be Function of S, the carrier of R;
  cluster Net-Str(S,f) -> transitive;
  coherence
  proof
    set N = Net-Str(S,f);
    let x,y,z be Element of N;
    assume that
A1: x <= y and
A2: y <= z;
A3: N.x <= N.y by A1,Def10;
    N.y <= N.z by A2,Def10;
    then N.x <= N.z by A3,YELLOW_0:def 2;
    hence thesis by Def10;
  end;
end;

registration
  let R be reflexive non empty RelStr;
  let S be non empty set, f be Function of S, the carrier of R;
  cluster Net-Str(S,f) -> reflexive;
  coherence
  proof
    let x be Element of Net-Str(S,f);
    Net-Str(S,f).x <= Net-Str(S,f).x;
    hence thesis by Def10;
  end;
end;

theorem 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;
  reconsider UN as universal set;
  the_transitive-closure_of the carrier of R in UN by CLASSES1:2;
  then the carrier of R in UN by CLASSES1:3,52;
  then
A3: S in UN by A1,CLASSES1:def 1;
  the carrier of N = S by Def10;
  hence thesis by A3,YELLOW_6:def 11;
end;

registration
  let R be LATTICE;
  cluster monotone reflexive strict for net of R;
  existence
  proof
    reconsider f = id the carrier of R
    as Function of the carrier of R, the carrier of R;
    rng f = [#]R by RELAT_1:45;
    then reconsider N = Net-Str(the carrier of R,f) as strict reflexive net of
    R by Th20;
    take N;
    thus thesis;
  end;
end;

defpred P[set] means not contradiction;

theorem 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;
  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 j9 = j as Element of N;
      j9 <= j9;
      then N.j9 in Y;
      hence thesis by A3;
    end;
    hence thesis by A2,YELLOW_0:33;
  end;
  rng the mapping of N = { G(j) where j is Element of N: P[j]} by Th19
    .= X from FRAENKEL:sch 5(A1);
  hence lim_inf N = Sup the mapping of N by YELLOW_2:def 5
    .= sup N by WAYBEL_2:def 1;
end;

theorem 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 = the set of all "/\"({N.i where i is Element of N:
  i >= j},R) where j is Element of N;
  set j = the Element of N;
A1: N.j is_>=_than X
  proof
    let b be Element of R;
    assume b in X;
    then consider j0 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 3;
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:16
      .= N.j by YELLOW_6:16;
    hence thesis by A2,A4,YELLOW_2:22;
  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;
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:16
        .= N.i0 by YELLOW_6:16;
      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 3;
A11:  N.i0 in Y by A10;
      assume
A12:  c is_<=_than Y;
      N.j = the_value_of N by YELLOW_6:16
        .= N.i0 by YELLOW_6:16;
      hence thesis by A11,A12;
    end;
    hence thesis by A7,A8,YELLOW_0:33;
  end;
  thus the_value_of N = N.j by YELLOW_6:16
    .= lim_inf N by A1,A5,YELLOW_0:32;
end;

theorem Th24:
  for R being complete LATTICE, N being constant net of R
  holds the_value_of N is_S-limit_of N
by Th23;

definition
  let S be non empty 1-sorted, e be Element of S;
  func Net-Str e -> strict NetStr over S means
  :Def11:
  the carrier of it = {e} & the InternalRel of it = {[e,e]} &
  the mapping of it = id {e};
  existence
  proof
    e in {e} by TARSKI:def 1;
    then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3;
A1: dom id{e} = {e} by RELAT_1:45;
    rng id{e} = {e} by RELAT_1:45;
    then reconsider f = id{e} as Function of {e}, the carrier of S
    by A1,RELSET_1:4;
    take NetStr(#{e},r,f#);
    thus thesis;
  end;
  uniqueness;
end;

registration
  let S be non empty 1-sorted, e be Element of S;
  cluster Net-Str e -> non empty;
  coherence
  proof
    set N = Net-Str e;
    the carrier of N = {e} by Def11;
    hence the carrier of N is non empty;
  end;
end;

theorem 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;
  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: the carrier of Net-Str e = {e} by Def11;
  then
A2: x = e by TARSKI:def 1;
  thus N.x = (id{e}).x by Def11
    .= e by A1,A2;
end;

registration
  let S be non empty 1-sorted, e be Element of S;
  cluster Net-Str e -> reflexive transitive directed antisymmetric;
  coherence
  proof
    set N = Net-Str e;
    the carrier of N = {e} by Def11;
    then reconsider e as Element of N by TARSKI:def 1;
    the InternalRel of N = {[e,e]} by Def11;
    then
A1: [e,e] in the InternalRel of N by TARSKI:def 1;
    thus N is reflexive
    proof
      let x be Element of N;
      x = e by Th25;
      hence thesis by A1,ORDERS_2:def 5;
    end;
    thus N is transitive
    proof
      let x,y,z be Element of N such that x <= y and y <= z;
A2:   x = e by Th25;
      z = e by Th25;
      hence thesis by A1,A2,ORDERS_2:def 5;
    end;
    thus N is directed
    proof
      let x,y be Element of N;
      take e;
A3:   x = e by Th25;
      y = e by Th25;
      hence thesis by A1,A3,ORDERS_2:def 5;
    end;
    let x,y be Element of N such that x <= y and y <= x;
    x = e by Th25;
    hence thesis by Th25;
  end;
end;

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

theorem 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 = the set of all "/\"({N.i where i is Element of N:
  i >= j},S) where j is Element of N;
  reconsider e9 = e as Element of S;
A1: X c= {e9}
  proof
    let u be object;
    assume u in X;
    then consider j 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= {e9}
    proof
      let v be object;
      assume v in Y;
      then consider i being Element of N such that
A4:   v = N.i and i >= j;
      reconsider i9 = i as Element of N;
      N.i9 = e by Th26;
      hence thesis by A4,TARSKI:def 1;
    end;
    reconsider j9 = j as Element of N;
    j9 <= j9;
    then N.j in Y;
    then Y = {e9} by A3,ZFMISC_1:33;
    then u = e9 by A2,YELLOW_0:39;
    hence thesis by TARSKI:def 1;
  end;
  set j = the Element of N;
  "/\"({N.i where i is Element of N: i >= j},S) in X;
  then X = {e9} by A1,ZFMISC_1:33;
  hence thesis by YELLOW_0:39;
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} by Def11;
  reconsider UN as universal set;
  the_transitive-closure_of the carrier of S in UN by CLASSES1:2;
  then the carrier of S in UN by CLASSES1:3,52;
  then the carrier of N in the_universe_of the carrier of S by A1,
CLASSES1:def 1;
  hence thesis by YELLOW_6:def 11;
end;

theorem Th30:
  for R being complete LATTICE, Z be net of R, D be Subset of R st
  D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
  where j is Element of Z holds D is non empty directed
proof
  let R be complete LATTICE, Z be net of R, D be Subset of R;
  assume
A1: D = the set of all "/\"({Z.k where k is Element of Z: k >= j},R)
  where j is Element of Z;
  set j = the 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 3;
  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 object;
    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 thesis by A6;
  end;
  hence x <= z by A2,WAYBEL_7:1;
  E c= Ey
  proof
    let e be object;
    assume e in E;
    then consider k 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 thesis by A8;
  end;
  hence y <= z by A3,WAYBEL_7:1;
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 24;
  let S be Subset of L;
  hereby
    assume S in the topology of T;
    then
A2: ex V being Subset of L st ( S = V)&( 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
A3:   sup D in S;
A4:   dom id D = D by RELAT_1:45;
A5:   rng id D = D by RELAT_1:45;
      then reconsider f = id D as Function of D, the carrier of L
      by A4,RELSET_1:4;
      reconsider N = Net-Str(D,f) as strict monotone reflexive net of L
      by A5,Th20;
A6:   N in NetUniv L by Th21;
      lim_inf N = sup N by Th22
        .= Sup the mapping of N by WAYBEL_2:def 1
        .= "\/"(rng the mapping of N,L) by YELLOW_2:def 5
        .= "\/"(rng f,L) by Def10
        .= sup D by RELAT_1:45;
      then sup D is_S-limit_of N;
      then [N,sup D] in SC by A6,Def8;
      then N is_eventually_in S by A2,A3;
      then consider i0 being Element of N such that
A7:   for j being Element of N st i0 <= j holds N.j in S;
      consider j0 being Element of N such that
A8:   j0 >= i0 and j0 >= i0 by YELLOW_6:def 3;
A9:   N.j0 in S by A7,A8;
A10:  D = the carrier of N by Def10;
      N.j0 = (id D).j0 by Def10
        .= j0 by A10;
      hence thesis by A9,A10,XBOOLE_0:3;
    end;
    thus S is upper
    proof
      let x,y be Element of L such that
A11:  x in S and
A12:  x <= y;
A13:  Net-Str y in NetUniv L by Th29;
      y = lim_inf Net-Str y by Th28;
      then x is_S-limit_of Net-Str y by A12;
      then [Net-Str y,x] in SC by A13,Def8;
      then Net-Str y is_eventually_in S by A2,A11;
      hence thesis by Th27;
    end;
  end;
  assume that
A14: S is inaccessible and
A15: S is upper;
  for p 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 p9 = p as Element of L;
    let N be net of L;
    assume
A17: [N,p] in SC;
    SC c= [:NetUniv L, the carrier of L:] by YELLOW_6:def 18;
    then
A18: N in NetUniv L by A17,ZFMISC_1:87;
    then ex N9 being strict net of L st N9 = N & the carrier of N9 in
    the_universe_of the carrier of L by YELLOW_6:def 11;
    then p is_S-limit_of N by A17,A18,Def8;
    then
A19: p9 <= lim_inf N;
    deffunc F(Element of N) = "/\"({N.i where i 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 DOMAIN_1:sch 8;
    then reconsider D = X as Subset of L;
    reconsider D as non empty directed Subset of L by Th30;
    sup D in S by A15,A16,A19;
    then D meets S by A14;
    then D /\ S <> {};
    then consider d being Element of L such that
A20: d in D /\ S by SUBSET_1:4;
    reconsider d as Element of L;
    d in D by A20,XBOOLE_0:def 4;
    then consider j 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 4;
    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:22;
    hence thesis by A15,A22;
  end;
  hence thesis 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;
  the topology of T = the topology of CSC
  proof
    thus the topology of T c= the topology of CSC
    proof
      let e be object;
      assume
A1:   e in the topology of T;
      then reconsider A = e as Subset of T;
      A is open by A1;
      then A is inaccessible upper by Def4;
      hence thesis by Th31;
    end;
    let e be object;
    assume
A2: e in the topology of CSC;
    then reconsider A = e as Subset of T by YELLOW_6:def 24;
    A is inaccessible upper by A2,Th31;
    then A is open by Def4;
    hence thesis;
  end;
  hence thesis by YELLOW_6:def 24;
end;

theorem 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 24;
  let S be Subset of T;
  hereby
    assume S is open;
    then S in the topology of T;
    then
A2: ex V being Subset of T st ( S = V)&( 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
A3:   sup D in S;
A4:   dom id D = D by RELAT_1:45;
A5:   rng id D = D by RELAT_1:45;
      then reconsider f = id D as Function of D, the carrier of T
      by A4,RELSET_1:4;
      reconsider N = Net-Str(D,f) as strict monotone reflexive net of T
      by A5,Th20;
A6:   N in NetUniv T by Th21;
      lim_inf N = sup N by Th22
        .= Sup the mapping of N by WAYBEL_2:def 1
        .= "\/"(rng the mapping of N,T) by YELLOW_2:def 5
        .= "\/"(rng f,T) by Def10
        .= sup D by RELAT_1:45;
      then sup D is_S-limit_of N;
      then [N,sup D] in SC by A6,Def8;
      then N is_eventually_in S by A2,A3;
      then consider i0 being Element of N such that
A7:   for j being Element of N st i0 <= j holds N.j in S;
      consider j0 being Element of N such that
A8:   j0 >= i0 and j0 >= i0 by YELLOW_6:def 3;
A9:   N.j0 in S by A7,A8;
A10:  D = the carrier of N by Def10;
      N.j0 = (id D).j0 by Def10
        .= j0 by A10;
      hence thesis by A9,A10,XBOOLE_0:3;
    end;
    thus S is upper
    proof
      let x,y be Element of T such that
A11:  x in S and
A12:  x <= y;
A13:  Net-Str y in NetUniv T by Th29;
      y = lim_inf Net-Str y by Th28;
      then x is_S-limit_of Net-Str y by A12;
      then [Net-Str y,x] in SC by A13,Def8;
      then Net-Str y is_eventually_in S by A2,A11;
      hence thesis by Th27;
    end;
  end;
  assume that
A14: S is inaccessible and
A15: S is upper;
  for p 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 p9 = p as Element of T;
    let N be net of T;
    assume
A17: [N,p] in SC;
    SC c= [:NetUniv T, the carrier of T:] by YELLOW_6:def 18;
    then
A18: N in NetUniv T by A17,ZFMISC_1:87;
    then ex N9 being strict net of T st N9 = N & the carrier of N9 in
    the_universe_of the carrier of T by YELLOW_6:def 11;
    then p is_S-limit_of N by A17,A18,Def8;
    then
A19: p9 <= lim_inf N;
    deffunc F(Element of N) = "/\"({N.i where i 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 DOMAIN_1:sch 8;
    then reconsider D = X as Subset of T;
    reconsider D as non empty directed Subset of T by Th30;
    sup D in S by A15,A16,A19;
    then D meets S by A14;
    then D /\ S <> {};
    then consider d being Element of T such that
A20: d in D /\ S by SUBSET_1:4;
    reconsider d as Element of T;
    d in D by A20,XBOOLE_0:def 4;
    then consider j 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 4;
    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:22;
    hence thesis by A15,A22;
  end;
  then S in the topology of T by A1;
  hence thesis;
end;

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

registration
  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 11;
    the_value_of M is_S-limit_of M by A2,Th24;
    hence thesis by A1,A2,Def8;
  end;
end;

registration
  let R be complete LATTICE;

:: 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 18;
    assume
A2: Y in NetUniv R;
    then consider Y9 being strict net of R such that
A3: Y9 = Y and the carrier of Y9 in the_universe_of the carrier of R
    by YELLOW_6:def 11;
    let p be Element of R;
    assume
A4: [N,p] in S;
    then
A5: N in NetUniv R by A1,ZFMISC_1:87;
    then consider N9 being strict net of R such that
A6: N9 = N and the carrier of N9 in the_universe_of the carrier of R
    by YELLOW_6:def 11;
    deffunc F(Element of N) = "/\"({N.i where i is Element of N: i >= $1},R);
    reconsider X1 = {F(j) where j is Element of N: P[j]}
    as Subset of R from DOMAIN_1:sch 8;
    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 DOMAIN_1:sch 8;
    p is_S-limit_of N9 by A4,A5,A6,Def8;
    then
A7: p <= lim_inf N by A6;
    consider f being Function 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 9;
    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 object;
        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 = N.(f.m) by A8,A12,FUNCT_2:15;
        hence thesis by A14;
      end;
      hence a <= b by A10,WAYBEL_7:1;
    end;
    then "\/"(X1,R) <= "\/"(X2,R) by Th2;
    then p <= lim_inf Y by A7,YELLOW_0:def 2;
    then p is_S-limit_of Y9 by A3;
    hence thesis by A2,A3,Def8;
  end;
end;

theorem 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 10;
  then
A2: (the mapping of N).j in X by FUNCT_1:def 7;
  the mapping of M = (the mapping of N)|the carrier of M by A1,YELLOW_6:def 6;
  hence thesis by A2,FUNCT_1:49;
end;

definition
  let L be non empty reflexive RelStr;
  func sigma L -> Subset-Family of L equals
  the topology of ConvergenceSpace Scott-Convergence L;
  coherence by YELLOW_6:def 24;
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:53;
    d in W by A2;
    hence thesis by A1,XBOOLE_0:3;
  end;
  hence thesis 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;
  set CSC = ConvergenceSpace Scott-Convergence T;
  assume the topology of T = sigma T;
  then the TopStruct of T =
  TopStruct(#the carrier of CSC, the topology of CSC#) by YELLOW_6:def 24;
  hence thesis by Th34;
end;

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

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;

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

Lm6: for T1,T2 being non empty 1-sorted, X be set
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;
  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;
  reconsider ii = i as Element of N2 by A1;
  take ii;
  let jj be Element of N2;
  reconsider j = jj as Element of N1 by A1;
  assume
A3: ii <= jj;
  N2.jj = N1.j by A1;
  hence thesis by A1,A2,A3;
end;

Lm7: for T1,T2 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:22;
    reconsider H = G as Subset of T1 by A1;
    G in the topology of T2 by A5;
    then H is open by A1;
    then p1 in Int W by A3,A6,A7,TOPS_1:22;
    then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def 1;
    thus N2 is_eventually_in V
    proof
      N1 is_eventually_in W by A4,YELLOW_6:def 15;
      then consider i being Element of N1 such that
A8:   for j being Element of N1 st i <= j holds N1.j in W;
      reconsider ii = i as Element of N2 by A2;
      take ii;
      let jj be Element of N2;
      reconsider j = jj as Element of N1 by A2;
      assume
A9:   ii <= jj;
      N2.jj = N1.j by A2;
      hence thesis by A2,A8,A9;
    end;
  end;
  hence thesis by YELLOW_6:def 15;
end;

Lm8: for T1,T2 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 18;
A3: Convergence T2 c= [:NetUniv T2,the carrier of T2:] by YELLOW_6:def 18;
  let u1,u2 be object;
  hereby
    assume
A4: [u1,u2] in Convergence T1;
    then consider N1 being Element of NetUniv T1, p1 being Point of T1
    such that
A5: [u1,u2] = [N1,p1] by A2,DOMAIN_1:1;
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 11;
    then reconsider N1 as net of T1;
A7: p1 in Lim N1 by A4,A5,YELLOW_6:def 19;
    reconsider N2 = N1 as net of T2 by A1;
    reconsider p2 =p1 as Point of T2 by A1;
A8: N2 in NetUniv T2 by A1,A6,Lm5;
    p2 in Lim N2 by A1,A7,Lm7;
    hence [u1,u2] in Convergence T2 by A5,A8,YELLOW_6:def 19;
  end;
  assume
A9: [u1,u2] in Convergence T2;
  then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that
A10: [u1,u2] = [N1,p1] by A3,DOMAIN_1:1;
A11: 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 11;
  then reconsider N1 as net of T2;
A12: p1 in Lim N1 by A9,A10,YELLOW_6:def 19;
  reconsider N2 = N1 as net of T1 by A1;
  reconsider p2 =p1 as Point of T1 by A1;
A13: N2 in NetUniv T1 by A1,A11,Lm5;
  p2 in Lim N2 by A1,A12,Lm7;
  hence thesis by A10,A13,YELLOW_6:def 19;
end;

Lm9: for R1,R2 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 x9 = x, y9 = y as Element of R1 by A1;
    consider z9 being Element of R1 such that
A4: z9 <= x9 and
A5: z9 <= y9 and
A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds w9 <= z9
    by A2,LATTICE3:def 11;
    reconsider z = z9 as Element of R2 by A1;
    take z;
    thus z <= x & z <= y by A1,A4,A5,Lm1;
    let w be Element of R2;
    reconsider w9 = w as Element of R1 by A1;
    assume that
A7: w <= x and
A8: w <= y;
A9: w9 <= x9 by A1,A7,Lm1;
    w9 <= y9 by A1,A8,Lm1;
    then w9 <= z9 by A6,A9;
    hence thesis by A1,Lm1;
  end;
A10: R2 is with_suprema
  proof
    let x,y be Element of R2;
    reconsider x9 = x, y9 = y as Element of R1 by A1;
    consider z9 being Element of R1 such that
A11: z9 >= x9 and
A12: z9 >= y9 and
A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds w9 >= z9
    by A2,LATTICE3:def 10;
    reconsider z = z9 as Element of R2 by A1;
    take z;
    thus z >= x & z >= y by A1,A11,A12,Lm1;
    let w be Element of R2;
    reconsider w9 = w as Element of R1 by A1;
    assume that
A14: w >= x and
A15: w >= y;
A16: w9 >= x9 by A1,A14,Lm1;
    w9 >= y9 by A1,A15,Lm1;
    then w9 >= z9 by A13,A16;
    hence thesis by A1,Lm1;
  end;
A17: R2 is reflexive
  by A1,A2,YELLOW_0:def 1,Lm1;
A18: R2 is transitive
  proof
    let x,y,z be Element of R2;
    reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1;
    assume that
A19: x <= y and
A20: y <= z;
A21: x9 <= y9 by A1,A19,Lm1;
    y9 <= z9 by A1,A20,Lm1;
    then x9 <= z9 by A2,A21,YELLOW_0:def 2;
    hence thesis by A1,Lm1;
  end;
  R2 is antisymmetric
  proof
    let x,y be Element of R2;
    reconsider x9 = x, y9 = y as Element of R1 by A1;
    assume that
A22: x <= y and
A23: y <= x;
A24: x9 <= y9 by A1,A22,Lm1;
    y9 <= x9 by A1,A23,Lm1;
    hence thesis by A2,A24,YELLOW_0:def 3;
  end;
  hence thesis by A3,A10,A17,A18;
end;

Lm10: for R1,R2 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
by Lm1;

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
by Lm1;

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 a9 = a as Element of R1 by A1;
    assume D is_<=_than a;
    then D is_<=_than a9 by A1,Lm10;
    then a9 >= "\/"(D,R1) by A3,YELLOW_0:def 9;
    hence thesis by A1,Lm1;
  end;
  hence thesis by A2,A4,YELLOW_0:def 9;
end;

Lm13: for R1,R2 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 a9 = a as Element of R1 by A1;
    assume D is_>=_than a;
    then D is_>=_than a9 by A1,Lm11;
    then a9 <= "/\"(D,R1) by A3,YELLOW_0:def 10;
    hence thesis by A1,Lm1;
  end;
  hence thesis by A2,A4,YELLOW_0:def 10;
end;

Lm14: for R1,R2 being non empty reflexive RelStr
st the RelStr of R1 = the RelStr of R2
for D being Subset of R1, D9 being Subset of R2 st D = D9 & D is directed
holds D9 is directed
proof
  let R1,R2 be non empty reflexive RelStr such that
A1: the RelStr of R1 = the RelStr of R2;
  let D be Subset of R1, D9 be Subset of R2 such that
A2: D = D9 and
A3: D is directed;
  let x2,y2 be Element of R2 such that
A4: x2 in D9 and
A5: y2 in D9;
  reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
  consider z1 being Element of R1 such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2,A3,A4,A5;
  reconsider z2 = z1 as Element of R2 by A1;
  take z2;
  thus z2 in D9 by A2,A6;
  thus x2 <= z2 & y2 <= z2 by A1,A7,A8,Lm1;
end;

Lm15: for R1,R2 being complete LATTICE st the RelStr of R1 = the RelStr of R2
for p,q being Element of R1 st p << q
for p9,q9 being Element of R2 st p = p9 & q = q9 holds p9 << q9
proof
  let R1,R2 be complete LATTICE such that
A1: the RelStr of R1 = the RelStr of R2;
  let p,q be Element of R1 such that
A2: p << q;
  let p9,q9 be Element of R2 such that
A3: p = p9 and
A4: q = q9;
  let D9 be non empty directed Subset of R2 such that
A5: q9 <= sup D9;
  reconsider D = D9 as non empty Subset of R1 by A1;
  reconsider D as non empty directed Subset of R1 by A1,Lm14;
  sup D = sup D9 by A1,Lm12;
  then q <= sup D by A1,A4,A5,Lm1;
  then consider d be Element of R1 such that
A6: d in D and
A7: p <= d by A2;
  reconsider d9 = d as Element of R2 by A1;
  take d9;
  thus d9 in D9 by A6;
  thus thesis by A1,A3,A7,Lm1;
end;

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

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

Lm18: for R1,R2 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 12;
    N is NetStr over R2 by A1;
    hence thesis;
  end;
  hence thesis by YELLOW_6:def 12;
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 18;
  for e being object st e in Scott-Convergence R1
    holds e in Scott-Convergence R2
  proof
    let e be object;
    assume
A3: e in Scott-Convergence R1;
    then consider N1 being Element of NetUniv R1,
    p1 being Element of R1 such that
A4: e = [N1,p1] by A2,DOMAIN_1:1;
A5: N1 in NetUniv R1;
A6: ex N being strict net of R1 st ( N1 = N)&( the carrier of N
    in the_universe_of the carrier of R1) by YELLOW_6:def 11;
    then reconsider N2 = N1 as strict net of R2 by A1,Lm4;
    reconsider N1 as strict net of R1 by A6;
    reconsider p2 = p1 as Element of R2 by A1;
A7: N2 in NetUniv R2 by A1,A5,Lm5;
A8: lim_inf N1 = lim_inf N2 by A1,Lm16;
    p1 is_S-limit_of N1 by A3,A4,Def8;
    then p1 <= lim_inf N1;
    then p2 <= lim_inf N2 by A1,A8,Lm1;
    then p2 is_S-limit_of N2;
    hence thesis by A4,A7,Def8;
  end;
  hence thesis;
end;

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

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 24;
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 24;
  the topology of T1 = the topology of T2
  proof
    thus the topology of T1 c= the topology of T2
    proof
      let e be object;
      assume e in the topology of T1;
      then consider V1 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;
        hence thesis by A5,A6,Lm6;
      end;
      hence thesis by A3,A4;
    end;
    let e be object;
    assume e in the topology of T2;
    then consider V1 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;
      hence thesis by A8,A9,Lm6;
    end;
    hence thesis by A2,A7;
  end;
  hence thesis;
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;
  reconsider a2 = a1 as Element of R2 by A1;
  take a2;
  thus X is_<=_than a2 by A1,A3,Lm10;
  let b2 be Element of R2;
  reconsider b1 = b2 as Element of R1 by A1;
  assume X is_<=_than b2;
  then X is_<=_than b1 by A1,Lm10;
  hence a2 <= b2 by A1,A4,Lm1;
end;

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

registration
  let R be continuous complete LATTICE;

:: 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 p9 = 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 11;
      not p is_S-limit_of N by A1,A2,A4,Def8;
      then not p <= lim_inf X by A4;
      then consider u being Element of R such that
A5:   u << p9 and
A6:   not u <= lim_inf X by A3,WAYBEL_3:24;
      set A = { a where a 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 = the set of all "/\"({X.k where k is Element of X:
        k >= j},R) where j is Element of X;
        "/\"(B,R) in C;
        then "/\"(B,R) <= lim_inf X by YELLOW_2:22;
        then not u <= "/\"(B,R) by A6,YELLOW_0:def 2;
        then not u is_<=_than B by YELLOW_0:33;
        then consider b being Element of R such that
A7:     b in B and
A8:     not u <= b;
        consider j being Element of X such that
A9:     b = X.j and
A10:    j >= i by A7;
        take j;
        thus i <= j by A10;
        thus thesis by A8,A9;
      end;
      then reconsider Y = X"A as subnet of X by YELLOW_6:22;
      take Y;
      reconsider UN = the_universe_of the carrier of R as universal set;
A11:  ex N being strict net of R st X = N &
      the carrier of N in UN by A1,YELLOW_6:def 11;
      X"A is SubRelStr of X by YELLOW_6:def 6;
      then the carrier of X"A c= the carrier of X by YELLOW_0:def 13;
      then the carrier of Y in UN by A11,CLASSES1:def 1;
      hence Y in NetUniv R by YELLOW_6:def 11;
      let Z be subnet of Y;
      assume
A12:  [Z,p] in C;
      C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18;
      then
A13:  Z in NetUniv R by A12,ZFMISC_1:87;
      then consider ZZ being strict net of R such that
A14:  ZZ = Z and the carrier of ZZ in UN by YELLOW_6:def 11;
      deffunc F(Element of Z)
      = "/\"({Z.i where i is Element of Z: i >= $1},R);
      set D = {F(j) where j is Element of Z: P[j]};
      D is Subset of R from DOMAIN_1:sch 8;
      then reconsider D as Subset of R;
      reconsider D as non empty directed Subset of R by Th30;
      p is_S-limit_of ZZ by A12,A13,A14,Def8;
      then p <= lim_inf Z by A14;
      then consider d being Element of R such that
A15:  d in D and
A16:  u <= d by A5;
      consider j being Element of Z such that
A17:  d = "/\"({Z.k where k is Element of Z: k >= j},R) by A15;
      reconsider j9 = j as Element of Z;
      consider i being Element of Z such that
A18:  i >= j9 and i >= j9 by YELLOW_6:def 3;
      consider f being Function of Z, Y such that
A19:  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 9;
      Z.i in {Z.k where k is Element of Z: k >= j} by A18;
      then
A20:  d <= Z.i by A17,YELLOW_2:22;
      Y.(f.i) = Z.i by A19,FUNCT_2:15;
      then Z.i in A by Th35;
      then ex a being Element of R st a = Z.i & not a >= u;
      hence contradiction by A16,A20,YELLOW_0:def 2;
    end;
    thus C is (ITERATED_LIMITS)
    proof
      let X be net of R, p be Element of R such that
A21:  [X,p] in C;
      let J be net_set of the carrier of X, R such that
A22:  for i being Element of X holds [J.i,X.i] in C;
A23:  C c= [:NetUniv R,the carrier of R:] by YELLOW_6:def 18;
      then
A24:  X in NetUniv R by A21,ZFMISC_1:87;
      for i being Element of X holds J.i in NetUniv R
      proof
        let i be Element of X;
        [J.i,X.i] in C by A22;
        hence thesis by A23,ZFMISC_1:87;
      end;
      then
A25:  Iterated J in NetUniv R by A24,YELLOW_6:25;
      reconsider p9 = p as Element of R;
      set q = lim_inf Iterated J;
      q is_>=_than waybelow p9
      proof
        let u be Element of R;
        assume u in waybelow p9;
        then
A26:    u << p9 by WAYBEL_3:7;
        set T = TopRelStr(#the carrier of R,the InternalRel of R, sigma R#);
A27:    the RelStr of T = the RelStr of R;
A28:    the carrier of R = the carrier of ConvergenceSpace C
        by YELLOW_6:def 24;
        then reconsider T as TopLattice by A27,Lm3,Lm9;
        reconsider T as complete TopLattice by A27,Lm22;
        reconsider T as continuous complete TopLattice by A27,Lm23;
        the topology of T = sigma T by A27,Lm21;
        then reconsider T as continuous complete Scott TopLattice by Th37;

:: 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 A27,Lm18;
        reconsider uu = u, qq = q, pp = p9 as Element of T;
        set N = Iterated JJ;
        set CC = Convergence T;
        CC = Convergence ConvergenceSpace C by A28,Lm8;
        then
A29:    C c= CC by YELLOW_6:40;
A30:    uu << pp by A26,A27,Lm15;
A31:    qq = lim_inf N by A27,Lm16,Lm17;
        for i 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;
          [J.ii,X.ii] in C by A22;
          hence thesis by A29;
        end;
        then [N,pp] in CC by A21,A29,YELLOW_6:def 23;
        then
A32:    pp in Lim N by YELLOW_6:def 19;
        pp in wayabove uu by A30;
        then wayabove uu is a_neighborhood of pp by Th36,CONNSP_2:3;
        then
A33:    N is_eventually_in wayabove uu by A32,YELLOW_6:def 15;
        wayabove uu c= uparrow uu by WAYBEL_3:11;
        then N is_eventually_in uparrow uu by A33,WAYBEL_0:8;
        hence u <= q by A27,A31,Lm1,Th18;
      end;
      then sup waybelow p9 <= q by YELLOW_0:32;
      then p <= q by WAYBEL_3:def 5;
      then p is_S-limit_of Iterated J;
      hence thesis by A25,Def8;
    end;
  end;
end;

theorem :: 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:44;
  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 11;
  the TopStruct of T = ConvergenceSpace Scott-Convergence T by Th32;
  then
A4: Convergence T = Convergence ConvergenceSpace Scott-Convergence T by Lm8;
  thus x is_S-limit_of N implies x in Lim N
  proof
    assume x is_S-limit_of N;
    then [N,x] in Convergence T by A1,A2,A3,A4,Def8;
    hence thesis by YELLOW_6:def 19;
  end;
  assume x in Lim N;
  then [M,x] in Scott-Convergence T by A1,A2,A3,A4,YELLOW_6:def 19;
  hence thesis by A1,A3,Def8;
end;

theorem 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;
    [:I,I:] c= [:I,I:];
    then reconsider r = [:I,I:] as Relation of I;
    dom F = I by PARTFUN1:def 2;
    then reconsider f = Sups F as Function of I, the carrier of L;
    set X = NetStr(#I,r,f#);
A6: for i,j 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:87;
      hence thesis by ORDERS_2:def 5;
    end;
A7: X is transitive
    by A6;
    X is directed
    proof
      let x,y be Element of X;
      take x;
      thus thesis by A6;
    end;
    then reconsider X = NetStr(#I,r,f#) as strict net of L by A7;
    deffunc F(Element of I) = Net-Str(K.$1,F.$1);
    consider J being ManySortedSet of I such that
A8: for i being Element of I holds J.i = F(i) from PBOOLE:sch 5;
    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 i9 = i as Element of I;
      reconsider rFi = rng(F.i9) as Subset of L;
A9:   rFi is directed by A4;
      J.i9 = Net-Str(K.i9,F.i9) by A8;
      hence thesis by A9,Th20;
    end;
    then reconsider J as net_set of the carrier of X, L by YELLOW_6:24;
A10: for j be set st j in I
    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 i9 = i as Element of I;
      take R = Net-Str(K.i9,F.i9);
      thus R = J.i by A8;
      thus thesis by Def10;
    end;
A11: doms F = K by YELLOW_7:45
      .= Carrier J by A10,PRALG_1:def 13;
A12: dom Frege F = product doms F by PARTFUN1:def 2;
    then
A13: dom Infs Frege F = product doms F by FUNCT_2:def 1;
A14: for i being Element of X holds J.i in NetUniv L
    proof
      let i be Element of X;
      reconsider i9 = i as Element of I;
A15:  J.i = Net-Str(K.i9,F.i9) by A8;
      then reconsider Ji = J.i as strict net of L;
      K.i9 in the_universe_of the carrier of L by A3;
      then the carrier of Ji in the_universe_of the carrier of L by A15,Def10;
      hence thesis by YELLOW_6:def 11;
    end;
A16: for i being Element of X holds [J.i,X.i] in C
    proof
      let i be Element of X;
      reconsider i9 = i as Element of I;
A17:  J.i = Net-Str(K.i9,F.i9) by A8;
      then reconsider Ji = J.i as monotone reflexive net of L;
A18:  J.i in NetUniv L by A14;
      i in I;
      then i9 in dom F by PARTFUN1:def 2;
      then X.i = Sup(F.i9) by WAYBEL_5:def 1
        .= Sup the mapping of Ji by A17,Def10
        .= sup Ji by WAYBEL_2:def 1
        .= lim_inf Ji by Th22;
      then X.i is_S-limit_of J.i;
      hence thesis by A17,A18,Def8;
    end;
A19: X in NetUniv L by A2,YELLOW_6:def 11;
    then
A20: Iterated J in NetUniv L by A14,YELLOW_6:25;
    deffunc I(Element of Iterated J) =
    {(Iterated J).p where p is Element of Iterated J :p >= $1};
    the carrier of Iterated J = [:the carrier of X, product Carrier J:]
    by YELLOW_6:26;
    then reconsider G = the mapping of Iterated J as
    Function of [:the carrier of X, product doms F:], the carrier of L by A11;
    deffunc I(Element of X, Element of product doms F) =
    {G.(i,$2) where i is Element of X :i >= $1};
    deffunc F(Element of product doms F) = "/\"(rng((Frege F).$1),L);
    deffunc F(Element of X, Element of product doms F) = "/\"(I($1,$2),L);
    set D = the set of all "/\"(I(j),L) where j is Element of Iterated J;
    set D9 = {F(i,g) where i is Element of X,
    g is Element of product doms F: P[g]};
    set E9 = {F(g) where g is Element of product doms F : P[g]};
A21: 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 object holds y in I(j,g) iff
      ex x being object st x in dom((Frege F).g) & y = ((Frege F).g).x
      proof
        let y be object;
        g in product Carrier J by A11;
        then
A22:    g in the carrier of product J by YELLOW_1:def 4;
        hereby
          assume y in I(j,g);
          then consider i being Element of X such that
A23:      y =G.(i,g) and i >= j;
          reconsider x = i as object;
          take x;
          reconsider i9 = i as Element of I;
A24:      i in I;
          then
A25:      i9 in dom F by PARTFUN1:def 2;
          thus x in dom((Frege F).g) by A24,PARTFUN1:def 2;
          thus ((Frege F).g).x = F.i9.(g.i) by A12,A25,WAYBEL_5:9
            .= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10
            .= (the mapping of J.i).(g.i) by A8
            .= y by A22,A23,YELLOW_6:def 13;
        end;
        given x being object such that
A26:    x in dom((Frege F).g) and
A27:    y = ((Frege F).g).x;
A28:    x in dom F by A12,A26,WAYBEL_5:8;
        reconsider i9 = x as Element of I by A26;
        reconsider i = i9 as Element of X;
A29:    i >= j by A6;
        y = (F.x).(g.x) by A12,A27,A28,WAYBEL_5:9
          .= (the mapping of Net-Str(K.i9,F.i9)).(g.i) by Def10
          .= (the mapping of J.i).(g.i) by A8
          .= G.(i,g) by A22,YELLOW_6:def 13;
        hence thesis by A29;
      end;
      hence thesis by FUNCT_1:def 3;
    end;
A30: D = D9
    proof
A31:  the carrier of Iterated J = [:the carrier of X, product Carrier J:]
      by YELLOW_6:26;
A32:  for p 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 13;
        reconsider g9 = g as Element of product J by A11,YELLOW_1:def 4;
        g9 in the carrier of product J;
        then
A35:    g9 in product Carrier J by YELLOW_1:def 4;
        reconsider i9 = i as Element of X;
        for i be object st i in the carrier of X
        ex R being RelStr, xi,yi being Element of R
        st R = J.i & xi = g9.i & yi = g9.i & xi <= yi
        proof
          let i be object;
          assume i in the carrier of X;
          then reconsider ii = i as Element of X;
          reconsider i9 = ii as Element of I;
A36:      J.i = Net-Str(K.i9,F.i9) by A8;
          set R = Net-Str(K.i9,F.i9);
          g9.ii in the carrier of R by A36;
          then reconsider x = g9.i as Element of R;
          take R,x,x;
          x <= x;
          hence thesis by A8;
        end;
        then
A37:    g9 <= g9 by A35,YELLOW_1:def 4;
        I(i,g) c= I(p)
        proof
          let u be object;
          assume u in I(i,g);
          then consider j being Element of X such that
A38:      u = (the mapping of Iterated J).(j,g) and
A39:      j >= i;
          reconsider j9 = j as Element of X;
          reconsider q = [j,g] as Element of Iterated J by A11,YELLOW_6:26;
          [j9,g9] >= [i9,g9] by A37,A39,YELLOW_3:11;
          then
A40:      q >= p by A33,A34,Lm1;
          u = (Iterated J).q by A38;
          hence thesis by A40;
        end;
        then
A41:    "/\"(I(p),L) <= "/\"(I(i,g),L) by WAYBEL_7:1;
        defpred P[Element of X] means $1 >= i;
        deffunc F(Element of X) = G.($1,g);
        {F(k) where k is Element of X: P[k]}
        is Subset of L from DOMAIN_1:sch 8;
        then reconsider A = I(i,g) as Subset of L;
        defpred P[Element of Iterated J] means $1 >= p;
        deffunc F(Element of Iterated J) = (Iterated J).$1;
        {F(z) where z is Element of Iterated J: P[z]}
        is Subset of L from DOMAIN_1:sch 8;
        then reconsider B = I(p) as Subset of L;
        B is_coarser_than A
        proof
          let b be Element of L;
          assume b in B;
          then consider q 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:1;
          reconsider k9 = k as Element of X;
          set a = (the mapping of Iterated J).(k,g);
          a = G.(k,g);
          then reconsider a as Element of L;
          take a;
          reconsider f9 = f as Element of product J by YELLOW_1:def 4;
A45:      [k9,f9] >= [i9,g9] by A33,A34,A43,A44,Lm1;
          then i <= k by YELLOW_3:11;
          hence a in A;
          reconsider k9 = k as Element of I;
          set N = Net-Str(K.k9,F.k9);
A46:      J.k = N by A8;
          reconsider g9k =g9.k, f9k = f9.k as Element of N by A8;
A47:      b = N.(f9k) by A42,A44,A46,YELLOW_6:27;
          reconsider kg = [k,g] as Element of Iterated J by A11,YELLOW_6:26;
A48:      a = (Iterated J).kg .= N.(g9k) by A46,YELLOW_6:27;
          g9 <= f9 by A45,YELLOW_3:11;
          then g9.k <= f9.k by WAYBEL_3:28;
          hence a <= b by A46,A47,A48,Def10;
        end;
        then "/\"(I(i,g),L) <= "/\"(I(p),L) by Th1;
        hence thesis by A41,YELLOW_0:def 3;
      end;
      thus D c= D9
      proof
        let e be object;
        assume e in D;
        then consider p 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:1;
        e = "/\"(I(j,g),L) by A32,A49,A50;
        hence thesis;
      end;
      let e be object;
      assume e in D9;
      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,YELLOW_6:26;
      e = "/\"(I(j),L) by A32,A51;
      hence thesis;
    end;
A52: E9 = D9 from Irrel(A21); :: UWAGA!!! wrazliwy na strony rownosci
    for y being object holds y in E9 iff
    ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x
    proof
      let y be object;
      thus y in E9 implies
      ex x being object st x in dom(Infs Frege F) & y = (Infs Frege F).x
      proof
        assume y in E9;
        then consider g being Element of product doms F such that
A53:    y = "/\"(rng((Frege F).g),L);
        take g;
        thus
A54:    g in dom(Infs Frege F) by A13;
        thus y = //\((Frege F).g, L) by A53,YELLOW_2:def 6
          .= (Infs Frege F).g by A54,WAYBEL_5:def 2;
      end;
      given x being object such that
A55:  x in dom(Infs Frege F) and
A56:  y = (Infs Frege F).x;
      reconsider x as Element of product doms F by A55,PARTFUN1:def 2;
      y = //\((Frege F).x, L) by A55,A56,WAYBEL_5:def 2
        .= "/\"(rng((Frege F).x),L) by YELLOW_2:def 6;
      hence thesis;
    end;
    then rng Infs Frege F = E9 by FUNCT_1:def 3;
    then
A57: Sup Infs Frege F = lim_inf Iterated J by A30,A52,YELLOW_2:def 5;
    reconsider x9 = x as Element of L;
    set X1 = the set of all x where j9 is Element of X;
    set X2 = the set of all "/\"({X.i where i is Element of X:i >= j},L)
    where j is Element of X;
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 object holds e in X3 iff
        ex u being object st u in dom Sups F & e = (Sups F).u
        proof
          let e be object;
          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 object;
            take u;
            u in I;
            hence u in dom Sups F by FUNCT_2:def 1;
            thus e = (Sups F).u by A60;
          end;
          given u being object such that
A61:      u in dom Sups F and
A62:      e = (Sups F).u;
          reconsider i = u as Element of X by A61,FUNCT_2:def 1;
A63:      i >= j by A6;
          e = X.i by A62;
          hence thesis by A63;
        end;
        then rng Sups F = X3 by FUNCT_1:def 3;
        hence thesis by YELLOW_2:def 6;
      end;
      thus X2 c= X1
      proof
        let u be object;
        assume u in X2;
        then ex j being Element of X st ( u = "/\"({X.i where i is
        Element of X:i >= j},L));
        then u = x by A59;
        hence thesis;
      end;
      let u be object;
      set j = the Element of X;
      assume u in X1;
      then ex j being Element of X st u = x;
      then u = "/\"({X.i where i is Element of X:i >= j},L) by A59;
      hence thesis;
    end;
    now
      let u be object;
      u in X1 iff ex j9 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 {x9} by A58,TARSKI:2
      .= x by YELLOW_0:39;
    then x <= lim_inf X;
    then x is_S-limit_of X;
    then [X,x] in C by A19,Def8;
    then [Iterated J,x] in C by A1,A16;
    then x is_S-limit_of Iterated J by A20,Def8;
    then x <= Sup Infs Frege F by A57;
    hence x = Sup Infs Frege F by A5,ORDERS_2:2;
  end;
  hence thesis by WAYBEL_5:18;
end;

theorem :: 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:44;
  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;
    d in S by A2,A5,WAYBEL_0:def 20;
    hence thesis by A4,XBOOLE_0:3;
  end;
  hence thesis 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 object;
  assume
A2: e in uparrow x;
  then reconsider y = e as Element of L;
  x <= y by A2,WAYBEL_0:18;
  hence thesis by A1,WAYBEL_0:def 20;
end;

theorem 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;
  then (waybelow p) /\ S <> {};
  then consider u being Element of L such that
A4: u in (waybelow p) /\ S by SUBSET_1:4;
  reconsider u as Element of L;
  take u;
  u in waybelow p by A4,XBOOLE_0:def 4;
  hence u << p by WAYBEL_3:7;
  thus thesis by A4,XBOOLE_0:def 4;
end;

theorem 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 object;
    assume e in X;
    then ex q being Element of L st e = wayabove q & q << p;
    hence thesis;
  end;
  then reconsider X as Subset-Family of L;
  X is Basis of p
  proof
A1: X is open
    proof
      let e be Subset of L;
      assume e in X;
      then consider q being Element of L such that
A2:   e = wayabove q and q << p;
      wayabove q is open by Th36;
      hence thesis by A2;
    end;
    X is p-quasi_basis
    proof
    for Y 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 thesis;
    end;
    hence p in Intersect X by SETFAM_1:43;
    let S be Subset of L such that
A3: S is open and
A4: p in S;
    consider u being Element of L such that
A5: u << p and
A6: u in S by A3,A4,Th43;
    take V = wayabove u;
    thus V in X by A5;
A7: S is upper by A3,Def4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
    uparrow u c= S by A6,A7,Th42;
    hence thesis by A8;
  end;
  hence thesis by A1;
  end;
  hence thesis;
end;

theorem Th45:
  for T being complete continuous Scott TopLattice holds
  the set of all  wayabove x where x is Element of T is Basis of T
proof
  let T be complete continuous Scott TopLattice;
  set B = the set of all  wayabove x where x is Element of T;
A1: B c= the topology of T
  proof
    let e be object;
    assume e in B;
    then consider x being Element of T such that
A2: e = wayabove x;
    wayabove x is open by Th36;
    hence thesis by A2;
  end;
  then reconsider P = B as Subset-Family of T by XBOOLE_1:1;
  for x 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 object;
    assume u in A;
    then ex q being Element of T st u = wayabove q & q << p;
    hence thesis;
  end;
  hence thesis by A1,YELLOW_8:14;
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 object;
    assume
A1: y in Int uparrow p;
    then reconsider q = y as Element of T;
    reconsider S = Int uparrow p as Subset of T;
    consider u being Element of T such that
A2: u << q and
A3: u in S by A1,Th43;
    S c= uparrow p by TOPS_1:16;
    then p <= u by A3,WAYBEL_0:18;
    then p << q by A2,WAYBEL_3:2;
    hence thesis;
  end;
  wayabove p c= uparrow p by WAYBEL_3:11;
  hence thesis by Th36,TOPS_1:24;
end;

theorem  :: 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 = the set of all  wayabove x where x is Element of T;
  set 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 object;
      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 thesis by A2,A4;
    end;
    let e be object;
    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 thesis by A5,A6;
  end;
  B is Basis of T by Th45;
  hence thesis by A1,YELLOW_8:11;
end;