let S, T be complete lower TopLattice; :: thesis: for f being Function of S,T st f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) holds
f is infs-preserving
let f be Function of S,T; :: thesis: ( f is continuous & ( for X being finite Subset of S holds f preserves_inf_of X ) implies f is infs-preserving )
assume f is continuous ; :: thesis: ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving )
then f is filtered-infs-preserving by Th11;
then for F being non empty filtered Subset of S holds f preserves_inf_of F ;
hence ( ex X being finite Subset of S st not f preserves_inf_of X or f is infs-preserving ) by WAYBEL_0:71; :: thesis: verum