for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N