theorem :: WAYBEL28:15

for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )