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 sigma R1 = sigma R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; :: thesis: sigma R1 = sigma R2
set T1 = ConvergenceSpace (Scott-Convergence R1);
set T2 = ConvergenceSpace (Scott-Convergence R2);
A2: the topology of (ConvergenceSpace (Scott-Convergence R1)) = { V where V is Subset of R1 : for p being Element of R1 st p in V holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V } by YELLOW_6:def 24;
A3: the topology of (ConvergenceSpace (Scott-Convergence R2)) = { V where V is Subset of R2 : for p being Element of R2 st p in V holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V } by YELLOW_6:def 24;
the topology of (ConvergenceSpace (Scott-Convergence R1)) = the topology of (ConvergenceSpace (Scott-Convergence R2))
proof
thus the topology of (ConvergenceSpace (Scott-Convergence R1)) c= the topology of (ConvergenceSpace (Scott-Convergence R2)) :: according to XBOOLE_0:def 10 :: thesis: the topology of (ConvergenceSpace (Scott-Convergence R2)) c= the topology of (ConvergenceSpace (Scott-Convergence R1))
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R1)) or e in the topology of (ConvergenceSpace (Scott-Convergence R2)) )
assume e in the topology of (ConvergenceSpace (Scott-Convergence R1)) ; :: thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R2))
then consider V1 being Subset of R1 such that
A4: e = V1 and
A5: for p being Element of R1 st p in V1 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V1 by A2;
reconsider V2 = V1 as Subset of R2 by A1;
for p being Element of R2 st p in V2 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V2
proof
let p2 be Element of R2; :: thesis: ( p2 in V2 implies for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2 )
assume A6: p2 in V2 ; :: thesis: for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R1 by A1;
let N2 be net of R2; :: thesis: ( [N2,p2] in Scott-Convergence R2 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R1 by A1;
assume [N2,p2] in Scott-Convergence R2 ; :: thesis: N2 is_eventually_in V2
then [N1,p1] in Scott-Convergence R1 by A1, Lm20;
hence N2 is_eventually_in V2 by A5, A6, Lm6; :: thesis: verum
end;
hence e in the topology of (ConvergenceSpace (Scott-Convergence R2)) by A3, A4; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R2)) or e in the topology of (ConvergenceSpace (Scott-Convergence R1)) )
assume e in the topology of (ConvergenceSpace (Scott-Convergence R2)) ; :: thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R1))
then consider V1 being Subset of R2 such that
A7: e = V1 and
A8: for p being Element of R2 st p in V1 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V1 by A3;
reconsider V2 = V1 as Subset of R1 by A1;
for p being Element of R1 st p in V2 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V2
proof
let p2 be Element of R1; :: thesis: ( p2 in V2 implies for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2 )
assume A9: p2 in V2 ; :: thesis: for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R2 by A1;
let N2 be net of R1; :: thesis: ( [N2,p2] in Scott-Convergence R1 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R2 by A1;
assume [N2,p2] in Scott-Convergence R1 ; :: thesis: N2 is_eventually_in V2
then [N1,p1] in Scott-Convergence R2 by A1, Lm20;
hence N2 is_eventually_in V2 by A8, A9, Lm6; :: thesis: verum
end;
hence e in the topology of (ConvergenceSpace (Scott-Convergence R1)) by A2, A7; :: thesis: verum
end;
hence sigma R1 = sigma R2 ; :: thesis: verum