:: deftheorem defines xi WAYBEL28:def 4 :
for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L));