:: deftheorem Def1 defines Homomorphism LATTICE4:def 1 :
for L1, L2 being Lattice
for b₃ being Function of the carrier of L1, the carrier of L2 holds
( b₃ is Homomorphism of L1,L2 iff for a1, b1 being Element of L1 holds
( b₃ . (a1 "\/" b1) = (b₃ . a1) "\/" (b₃ . b1) & b₃ . (a1 "/\" b1) = (b₃ . a1) "/\" (b₃ . b1) ) );