theorem Th26: :: WAYBEL28:26

for L being non empty complete LATTICE
for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L