for S, T being complete Scott TopLattice
for f being Function of S,T holds
( f is continuous iff for N being net of S holds f . (lim_inf N) <= lim_inf (f * N) ) by Lm4, Lm8, Lm9;