for L being complete LATTICE
for N being net of L holds inf N <= lim_inf N