for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )