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, WAYBEL_0:def 30;
hence f . (Top S) = Top T by RELAT_1:149; :: thesis: verum