theorem Th8: :: WAYBEL17:8

for S, T being with_infima Poset
for a, b being Element of S
for f being Function of S,T holds lim_inf (f * (Net-Str (a,b))) = (f . a) "/\" (f . b)