set C = Scott-Convergence R;
thus ( Scott-Convergence R is (CONSTANTS) & Scott-Convergence R is (SUBNETS) ) ; :: according to YELLOW_6:def 25 :: thesis:
thus Scott-Convergence R is (DIVERGENCE) :: thesis:

let X be net of R; :: according to YELLOW_6:def 22 :: thesis:
let p be Element of R; :: thesis:
assume that
A1: X in NetUniv R and
A2: not [X,p] in Scott-Convergence R ; :: thesis:
A3: for x being Element of R holds
( not waybelow x is empty & waybelow x is 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 where a is Element of R : not a >= u }

let i be Element of X; :: according to WAYBEL_0:def 12 :: thesis:
set B = { (X . j) where j is Element of X : j >= i } ;
set C = { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ;
"/\" ( { (X . j) where j is Element of X : j >= i } ,R) in { ("/\" ( { (X . k) where k is Element of X : k >= j } ,R)) where j is Element of X : verum } ;
then "/\" ( { (X . j) where j is Element of X : j >= i } ,R) <= lim_inf X by YELLOW_2:22;
then not u <= "/\" ( { (X . j) where j is Element of X : j >= i } ,R) by A6, YELLOW_0:def 2;
then not u is_<=_than { (X . j) where j is Element of X : j >= i } by YELLOW_0:33;
then consider b being Element of R such that
A7: b in { (X . j) where j is Element of X : j >= i } 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 ; :: thesis:
thus i <= j by A10; :: thesis:
thus X . j in { a where a is Element of R : not a >= u } by A8, A9; :: thesis:

end;

then reconsider Y = X " { a where a is Element of R : not a >= u } as subnet of X by YELLOW_6:22;
take Y ; :: thesis:
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 where a is Element of R : not a >= u } is SubRelStr of X by YELLOW_6:def 6;
then the carrier of (X " { a where a is Element of R : not a >= u } ) 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; :: thesis:
let Z be subnet of Y; :: thesis:
assume A12: [Z,p] in Scott-Convergence R ; :: thesis:
Scott-Convergence R 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 H₁( Element of Z) -> Element of the carrier of R = "/\" ( { (Z . i) where i is Element of Z : i >= R } ,R);
set D = { H₁(j) where j is Element of Z : S₁[j] } ;
{ H₁(j) where j is Element of Z : S₁[j] } is Subset of R from DOMAIN_1:sch 8();
then reconsider D = { H₁(j) where j is Element of Z : S₁[j] } as Subset of R ;
reconsider D = 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 where a is Element of R : not a >= u } 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; :: thesis:

end;

thus Scott-Convergence R is (ITERATED_LIMITS) :: thesis:

proof

let X be net of R; :: according to YELLOW_6:def 23 :: thesis:
let p be Element of R; :: thesis:
assume A21: [X,p] in Scott-Convergence R ; :: thesis:
let J be net_set of the carrier of X,R; :: thesis:
assume A22: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence R ; :: thesis:
A23: Scott-Convergence R 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; :: thesis:
[(J . i),(X . i)] in Scott-Convergence R by A22;
hence J . i in NetUniv R by A23, ZFMISC_1:87; :: thesis:

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);
lim_inf (Iterated J) is_>=_than waybelow p9

proof

let u be Element of R; :: according to LATTICE3:def 9 :: thesis:
assume u in waybelow p9 ; :: thesis:
then A26: u << p9 by WAYBEL_3:7;
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
A27: RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
A28: the carrier of R = the carrier of (ConvergenceSpace (Scott-Convergence R)) by YELLOW_6:def 24;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopLattice by A27, Lm3, Lm9;
reconsider T = T as complete TopLattice by A27, Lm22;
reconsider T = T as complete continuous TopLattice by A27, Lm23;
the topology of T = sigma T by A27, Lm21;
then reconsider T = T as complete continuous Scott TopLattice by Th37;
reconsider XX = X as net of T ;
reconsider JJ = J as net_set of the carrier of XX,T by A27, Lm18;
reconsider uu = u, qq = lim_inf (Iterated J), pp = p9 as Element of T ;
set N = Iterated JJ;
set CC = Convergence T;
Convergence T = Convergence (ConvergenceSpace (Scott-Convergence R)) by A28, Lm8;
then A29: Scott-Convergence R c= Convergence T by YELLOW_6:40;
A30: uu << pp by A26, A27, Lm15;
A31: qq = lim_inf (Iterated JJ) by A27, Lm16, Lm17;
for i being Element of XX holds [(JJ . i),(XX . i)] in Convergence T

proof

let i be Element of XX; :: thesis:
reconsider ii = i as Element of X ;
[(J . ii),(X . ii)] in Scott-Convergence R by A22;
hence [(JJ . i),(XX . i)] in Convergence T by A29; :: thesis:

end;

then [(Iterated JJ),pp] in Convergence T by A21, A29, YELLOW_6:def 23;
then A32: pp in Lim (Iterated JJ) 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: Iterated JJ is_eventually_in wayabove uu by A32, YELLOW_6:def 15;
wayabove uu c= uparrow uu by WAYBEL_3:11;
then Iterated JJ is_eventually_in uparrow uu by A33, WAYBEL_0:8;
hence u <= lim_inf (Iterated J) by A27, A31, Lm1, Th18; :: thesis:

end;

then sup (waybelow p9) <= lim_inf (Iterated J) by YELLOW_0:32;
then p <= lim_inf (Iterated J) by WAYBEL_3:def 5;
then p is_S-limit_of Iterated J ;
hence [(Iterated J),p] in Scott-Convergence R by A25, Def8; :: thesis:

end;