for L being complete LATTICE
for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D