let CL be C_Lattice; :: thesis: 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)
let IL be implicative Lattice; :: thesis: 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)
let f be Homomorphism of IL,CL; :: thesis: 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)
let i, j, k be Element of IL; :: thesis: ( f is one-to-one & (f . i) "/\" (f . k) [= f . j implies f . k [= f . (i => j) )
assume A1: f is one-to-one ; :: thesis: ( not (f . i) "/\" (f . k) [= f . j or f . k [= f . (i => j) )

hereby :: thesis: verum

assume (f . i) "/\" (f . k) [= f . j ; :: thesis: f . k [= f . (i => j)
then f . (i "/\" k) [= f . j by D2;
then i "/\" k [= j by A1, Th5;
then k [= i => j by FILTER_0:def 7;
hence f . k [= f . (i => j) by Th4; :: thesis: verum

end;