let T be complete Scott TopLattice; :: thesis: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
set CSC = ConvergenceSpace (Scott-Convergence T);
the topology of T = the topology of (ConvergenceSpace (Scott-Convergence T))

proof

thus the topology of T c= the topology of (ConvergenceSpace (Scott-Convergence T)) :: according to XBOOLE_0:def 10 :: thesis: the topology of (ConvergenceSpace (Scott-Convergence T)) c= the topology of T

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the topology of T or e in the topology of (ConvergenceSpace (Scott-Convergence T)) )
assume A1: e in the topology of T ; :: thesis: e in the topology of (ConvergenceSpace (Scott-Convergence T))
then reconsider A = e as Subset of T ;
A is open by A1;
then ( A is inaccessible & A is upper ) by Def4;
hence e in the topology of (ConvergenceSpace (Scott-Convergence T)) by Th31; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence T)) or e in the topology of T )
assume A2: e in the topology of (ConvergenceSpace (Scott-Convergence T)) ; :: thesis: e in the topology of T
then reconsider A = e as Subset of T by YELLOW_6:def 24;
( A is inaccessible & A is upper ) by A2, Th31;
then A is open by Def4;
hence e in the topology of T ; :: thesis: verum

end;

hence TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by YELLOW_6:def 24; :: thesis: verum