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