set S = Scott-Convergence R;
let N be net of ; :: according to YELLOW_6:def 24 :: thesis: for b₁ being subnet of N holds
( not b₁ in NetUniv R or for b₂ being Element of the carrier of R holds
( not [N,b₂] in Scott-Convergence R or [b₁,b₂] in Scott-Convergence R ) )
let Y be subnet of N; :: thesis: ( not Y in NetUniv R or for b₁ being Element of the carrier of R holds
( not [N,b₁] in Scott-Convergence R or [Y,b₁] in Scott-Convergence R ) )
A1: Scott-Convergence R c= [:(NetUniv R),the carrier of R:] by YELLOW_6:def 21;
assume A2: Y in NetUniv R ; :: thesis: for b₁ being Element of the carrier of R holds
( not [N,b₁] in Scott-Convergence R or [Y,b₁] in Scott-Convergence R )
then consider Y' being strict net of strict such that
A3: Y' = Y and
the carrier of Y' in the_universe_of the carrier of R by YELLOW_6:def 14;
let p be Element of ; :: 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:106;
then consider N' being strict net of strict such that
A6: N' = N and
the carrier of N' in the_universe_of the carrier of R by YELLOW_6:def 14;
deffunc H₁( Element of ) -> Element of the carrier of R = "/\" { (N . i) where i is Element of : i >= R } ,R;
defpred S₁[ set ] means verum;
reconsider X1 = { H₁(j) where j is Element of : S₁[j] } as Subset of from DOMAIN_1:sch 8();
deffunc H₂( Element of ) -> Element of the carrier of R = "/\" { (Y . i) where i is Element of : i >= R } ,R;
reconsider X2 = { H₂(j) where j is Element of : S₁[j] } as Subset of from DOMAIN_1:sch 8();
p is_S-limit_of N' by A4, A5, A6, Def8;
then A7: p <= lim_inf N by A6, Def7;
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 ex n being Element of st
for p being Element of st n <= p holds
m <= f . p by YELLOW_6:def 12;
X1 is_finer_than X2

proof

let a be Element of ; :: according to YELLOW_4:def 1 :: thesis: ( not a in X1 or ex b₁ being Element of the carrier of R st
( b₁ in X2 & a <= b₁ ) )
assume a in X1 ; :: thesis: ex b₁ being Element of the carrier of R st
( b₁ in X2 & a <= b₁ )
then consider j being Element of such that
A10: a = "/\" { (N . i) where i is Element of : i >= j } ,R ;
reconsider j = j as Element of ;
consider n being Element of such that
A11: for p being Element of st n <= p holds
j <= f . p by A9;
set X3 = { (Y . i) where i is Element of : i >= n } ;
set X4 = { (N . i) where i is Element of : i >= j } ;
take b = "/\" { (Y . i) where i is Element of : i >= n } ,R; :: thesis: ( b in X2 & a <= b )
thus b in X2 ; :: thesis: a <= b
{ (Y . i) where i is Element of : i >= n } c= { (N . i) where i is Element of : i >= j }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { (Y . i) where i is Element of : i >= n } or u in { (N . i) where i is Element of : i >= j } )
assume u in { (Y . i) where i is Element of : i >= n } ; :: thesis: u in { (N . i) where i is Element of : i >= j }
then consider m being Element of such that
A12: u = Y . m and
A13: m >= n ;
reconsider m = m as Element of ;
A14: f . m >= j by A11, A13;
u = N . (f . m) by A8, A12, FUNCT_2:21;
hence u in { (N . i) where i is Element of : i >= j } by A14; :: thesis: verum

end;

hence a <= b by A10, WAYBEL_7:3; :: 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 Y' by A3, Def7;
hence [Y,p] in Scott-Convergence R by A2, A3, Def8; :: thesis: verum