theorem Th11: :: WAYBEL17:11

for S, T being LATTICE
for f being Function of S,T st ( for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) holds
f is monotone