let S, T be non empty complete lower TopLattice; :: thesis: for f being Function of S,T st f is infs-preserving holds
f is continuous
let f be Function of S,T; :: thesis: ( f is infs-preserving implies f is continuous )
assume f is infs-preserving ; :: thesis: f is continuous
then for X being non empty Subset of S holds f preserves_inf_of X ;
hence f is continuous by Th8; :: thesis: verum