for T being complete LATTICE
for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N