for CL being C_Lattice
for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )