:: deftheorem defines preserves_implication LATTICE4:def 4 :
for L1, L2 being Lattice
for f being Homomorphism of L1,L2 holds
( f preserves_implication iff for a1, b1 being Element of L1 holds f . (a1 => b1) = (f . a1) => (f . b1) );