for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, j, k being Element of IL st f is one-to-one & (f . i) "/\" (f . k) [= f . j holds
f . k [= f . (i => j)