for R being complete LATTICE
for N being constant net of R holds the_value_of N = lim_inf N