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) )

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) )