let S, T be Semilattice; :: thesis: for f being Function of S,T st f is infs-preserving holds
f is SemilatticeHomomorphism of S,T
let f be Function of S,T; :: thesis: ( f is infs-preserving implies f is SemilatticeHomomorphism of S,T )
assume A1: f is infs-preserving ; :: thesis: f is SemilatticeHomomorphism of S,T
reconsider e = {} as Subset of S by XBOOLE_1:2;
hereby :: according to WAYBEL21:def 1 :: thesis: for X being finite Subset of S holds f preserves_inf_of X
assume S is upper-bounded ; :: thesis: T is upper-bounded
then A2: ex_inf_of e,S by YELLOW_0:43;
f preserves_inf_of e by A1;
then A3: ex_inf_of f .: e,T by A2;
f .: e = {} ;
hence T is upper-bounded by A3, WAYBEL20:5; :: thesis: verum
end;
let X be finite Subset of S; :: thesis: f preserves_inf_of X
thus f preserves_inf_of X by A1; :: thesis: verum