:: deftheorem Def8 defines Semilattice-Homomorphism VECTSP_8:def 8 :
for L1, L2 being Lattice
for b₃ being Function of the carrier of L1, the carrier of L2 holds
( b₃ is Semilattice-Homomorphism of L1,L2 iff for a, b being Element of L1 holds b₃ . (a "/\" b) = (b₃ . a) "/\" (b₃ . b) );