theorem Th3: :: WAYBEL28:3

for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )