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