:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def 3 :
for L being non empty RelStr
for b₂ being Convergence-Class of L holds
( b₂ = lim_inf-Convergence L iff for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b₂ iff for M being subnet of N holds x = lim_inf M ) );