let CL be C_Lattice; :: thesis: 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
let IL be implicative Lattice; :: thesis: for f being Homomorphism of IL,CL
for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
let f be Homomorphism of IL,CL; :: thesis: for i, j being Element of IL holds (f . i) "/\" (f . (i => j)) [= f . j
let i, j be Element of IL; :: thesis: (f . i) "/\" (f . (i => j)) [= f . j
i "/\" (i => j) [= j by FILTER_0:def 7;
then f . (i "/\" (i => j)) [= f . j by Th4;
hence (f . i) "/\" (f . (i => j)) [= f . j by D2; :: thesis: verum