theorem Th23: :: WAYBEL11:23

for R being complete LATTICE
for N being constant net of R holds the_value_of N = lim_inf N