let S, T be upper-bounded Semilattice; :: thesis: for f being SemilatticeHomomorphism of S,T holds f . (Top S) = Top T
let f be SemilatticeHomomorphism of S,T; :: thesis: f . (Top S) = Top T
A1: f preserves_inf_of {} S by Def1;
ex_inf_of {} S,S by YELLOW_0:43;
then f . (inf ({} S)) = inf (f .: ({} S)) by A1;
hence f . (Top S) = Top T ; :: thesis: verum