let L be complete Scott TopLattice; :: thesis: sigma L = the topology of L
TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
hence sigma L = the topology of L by WAYBEL11:def 12; :: thesis: verum