set S = Scott-Convergence R;
let N be net of R; :: according to YELLOW_6:def 21 :: thesis: for b1 being subnet of N holds
( not b1 in NetUniv R or for b2 being Element of the carrier of R holds
( not [N,b2] in Scott-Convergence R or [b1,b2] in Scott-Convergence R ) )
let Y be subnet of N; :: thesis: ( not Y in NetUniv R or for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R ) )
A1: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def 18;
assume A2: Y in NetUniv R ; :: thesis: for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence 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; :: thesis: ( not [N,p] in Scott-Convergence R or [Y,p] in Scott-Convergence R )
assume A4: [N,p] in Scott-Convergence R ; :: thesis: [Y,p] in Scott-Convergence R
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 H1( Element of N) -> Element of the carrier of R = "/\" ( { (N . i) where i is Element of N : i >= R } ,R);
reconsider X1 = { H1(j) where j is Element of N : S1[j] } as Subset of R from DOMAIN_1:sch 8();
 deffunc H2( Element of Y) -> Element of the carrier of R = "/\" ( { (Y . i) where i is Element of Y : i >= R } ,R);
reconsider X2 = { H2(j) where j is Element of Y : S1[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; :: according to YELLOW_4:def 1 :: thesis: ( not a in X1 or ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 ) )
assume a in X1 ; :: thesis: ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 )
then consider j being Element of N such that
A10: a = "/\" ( { (N . i) where i is Element of N : i >= j } ,R) ;
reconsider j = 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 } ;
set X4 = { (N . i) where i is Element of N : i >= j } ;
take b = "/\" ( { (Y . i) where i is Element of Y : i >= n } ,R); :: thesis: ( b in X2 & a <= b )
thus b in X2 ; :: thesis: a <= b
{ (Y . i) where i is Element of Y : i >= n } c= { (N . i) where i is Element of N : i >= j }
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { (Y . i) where i is Element of Y : i >= n } or u in { (N . i) where i is Element of N : i >= j } )
assume u in { (Y . i) where i is Element of Y : i >= n } ; :: thesis: u in { (N . i) where i is Element of N : i >= j }
then consider m being Element of Y such that
A12: u = Y . m and
A13: m >= n ;
reconsider m = m as Element of Y ;
A14: f . m >= j by A11, A13;
u = N . (f . m) by A8, A12, FUNCT_2:15;
hence u in { (N . i) where i is Element of N : i >= j } by A14; :: thesis: verum
end;
hence a <= b by A10, WAYBEL_7:1; :: thesis: verum
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 [Y,p] in Scott-Convergence R by A2, A3, Def8; :: thesis: verum