theorem Th26: :: LATTICE4:26

for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j