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 set ; :: 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 ;
A is open by A1, PRE_TOPC:def 5;
then ( A is inaccessible_by_directed_joins & A is upper ) by Def4;
hence e in the topology of (ConvergenceSpace (Scott-Convergence T)) by Th31; :: thesis: verum

end;

let e be set ; :: 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 by YELLOW_6:def 27;
( A is inaccessible_by_directed_joins & A is upper ) by A2, Th31;
then A is open by Def4;
hence e in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

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