for R being complete LATTICE
for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q