sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def 12;
hence not sigma L is empty ; :: thesis: verum