let CL be C_Lattice; :: thesis:
let IL be implicative Lattice; :: thesis:
let f be Homomorphism of IL,CL; :: thesis:
assume A1: f is bijective ; :: thesis:
thus CL is implicative :: thesis:

proof

let p, q be Element of CL; :: according to FILTER_0:def 6 :: thesis:
consider i being Element of IL such that
A2: f . i = p by A1, Th6;
consider j being Element of IL such that
A3: f . j = q by A1, Th6;
take r = f . (i => j); :: thesis:
thus p "/\" r [= q by A2, A3, Th26; :: thesis:

hereby :: thesis:

let r1 be Element of CL; :: thesis:
assume A4: p "/\" r1 [= q ; :: thesis:
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= r by A1, A2, A3, A4, Th27; :: thesis:

end;

end;

then reconsider CL = CL as implicative Lattice ;
reconsider f = f as Homomorphism of IL,CL ;

now :: thesis:

let i, j be Element of IL; :: thesis:

A5: now :: thesis:

let r1 be Element of CL; :: thesis:
assume A6: (f . i) "/\" r1 [= f . j ; :: thesis:
ex k being Element of IL st f . k = r1 by A1, Th6;
hence r1 [= f . (i => j) by A1, A6, Th27; :: thesis:

end;

(f . i) "/\" (f . (i => j)) [= f . j by Th26;
hence (f . i) => (f . j) = f . (i => j) by A5, FILTER_0:def 7; :: thesis:

end;

hence f preserves_implication ; :: thesis: