theorem :: WAYBEL28:13

for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L & x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) holds
( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) ) by Th10;