let R1, R2 be complete LATTICE; :: thesis: ( 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 #)
; :: thesis: Scott-Convergence R1 c= Scott-Convergence R2
A2:
Scott-Convergence R1 c= [:(NetUniv R1),the carrier of R1:]
by YELLOW_6:def 21;
for e being set st e in Scott-Convergence R1 holds
e in Scott-Convergence R2
proof
let e be
set ;
:: thesis: ( e in Scott-Convergence R1 implies e in Scott-Convergence R2 )
assume A3:
e in Scott-Convergence R1
;
:: thesis: 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:9;
A5:
N1 in NetUniv R1
;
consider N being
strict net of
R1 such that A6:
N1 = N
and
the
carrier of
N in the_universe_of the
carrier of
R1
by YELLOW_6:def 14;
reconsider N2 =
N1 as
strict net of
R2 by A1, A6, 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
by Def7;
then
p2 <= lim_inf N2
by A1, A8, Lm1;
then
p2 is_S-limit_of N2
by Def7;
hence
e in Scott-Convergence R2
by A4, A7, Def8;
:: thesis: verum
end;
hence
Scott-Convergence R1 c= Scott-Convergence R2
by TARSKI:def 3; :: thesis: verum