:: deftheorem Def1 defines SemilatticeHomomorphism WAYBEL21:def 1 :
for S, T being Semilattice st ( S is upper-bounded implies T is upper-bounded ) holds
for b₃ being Function of S,T holds
( b₃ is SemilatticeHomomorphism of S,T iff for X being finite Subset of S holds b₃ preserves_inf_of X );