for S being up-complete LATTICE
for D being non empty directed Subset of S holds lim_inf (Net-Str D) = sup D