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
A2: ex_inf_of f .: {},T by YELLOW_0:43;
( X = {} or f preserves_inf_of X ) by Th2;
hence f preserves_inf_of X by A1, A2; :: thesis: verum