let T be complete TopLattice; :: thesis: ( the topology of T = sigma T implies T is Scott )
set CSC = ConvergenceSpace (Scott-Convergence T);
assume the topology of T = sigma T ; :: thesis: T is Scott
then TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (ConvergenceSpace (Scott-Convergence T)), the topology of (ConvergenceSpace (Scott-Convergence T)) #) by YELLOW_6:def 24;
hence T is Scott by Th34; :: thesis: verum