let R1, R2 be complete LATTICE; ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 c= Scott-Convergence R2 )
assume A1:
RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #)
; Scott-Convergence R1 c= Scott-Convergence 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 ;
( e in Scott-Convergence R1 implies e in Scott-Convergence R2 )
assume A3:
e in Scott-Convergence R1
;
e in Scott-Convergence R2
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 =
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
e in Scott-Convergence R2
by A4, A7, Def8;
verum
end;
hence
Scott-Convergence R1 c= Scott-Convergence R2
; verum