let S, T be upper-bounded Semilattice; :: thesis: for f being meet-preserving Function of S,T st f . (Top S) = Top T holds
f is SemilatticeHomomorphism of S,T
let f be meet-preserving Function of S,T; :: thesis: ( f . (Top S) = Top T implies f is SemilatticeHomomorphism of S,T )
assume A1: f . (Top S) = Top T ; :: thesis: f is SemilatticeHomomorphism of S,T
thus ( S is upper-bounded implies T is upper-bounded ) ; :: according to WAYBEL21:def 1 :: thesis: for X being finite Subset of S holds f preserves_inf_of X
let X be finite Subset of S; :: thesis: f preserves_inf_of X
( f .: {} = {} & Top S = "/\" {} ,S ) by RELAT_1:149;
then A2: ( ex_inf_of f .: {} ,T & "/\" (f .: {} ),T = f . ("/\" {} ,S) ) by A1, YELLOW_0:43;
( X = {} or f preserves_inf_of X ) by Th2;
hence f preserves_inf_of X by A2, WAYBEL_0:def 30; :: thesis: verum