let T be complete Scott TopLattice; :: thesis: ( T is continuous iff Convergence T = Scott-Convergence T )
hereby :: thesis: ( Convergence T = Scott-Convergence T implies T is continuous )
assume T is continuous ; :: thesis: Convergence T = Scott-Convergence T
then reconsider L = T as complete continuous Scott TopLattice ;
TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
hence Convergence T = Convergence (ConvergenceSpace (Scott-Convergence L)) by Lm8
.= Scott-Convergence T by YELLOW_6:44 ;
:: thesis: verum
end;
thus ( Convergence T = Scott-Convergence T implies T is continuous ) by Th39; :: thesis: verum