:: deftheorem defines sigma WAYBEL11:def 12 :
for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));