let T be complete TopLattice; :: thesis: ( TopStruct(# the carrier of T,the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies T is Scott )
assume TopStruct(# the carrier of T,the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; :: thesis: T is Scott
hence for S being Subset of T holds
( S is open iff ( S is inaccessible_by_directed_joins & S is upper ) ) by Th33; :: according to WAYBEL11:def 4 :: thesis: verum