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
( f preserves_inf_of {} S & ex_inf_of {} S,S ) by Def1, YELLOW_0:43;
then f . (inf ({} S)) = inf (f .: ({} S)) by WAYBEL_0:def 30;
hence f . (Top S) = Top T by RELAT_1:149; :: thesis: verum