theorem Th24: :: WAYBEL32:24

for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N