for L1, L2 being Lattice
for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1 by D1;