for T being complete LATTICE
for N being net of T
for M being subnet of N holds lim_inf N <= lim_inf M