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

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