let CL be C_Lattice; :: thesis: for IL being implicative Lattice
for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )

let IL be implicative Lattice; :: thesis: for f being Homomorphism of IL,CL st f is bijective holds
( CL is implicative & f preserves_implication )

let f be Homomorphism of IL,CL; :: thesis: ( f is bijective implies ( CL is implicative & f preserves_implication ) )
assume A1: f is bijective ; :: thesis: ( CL is implicative & f preserves_implication )
thus CL is implicative :: thesis:
proof
let p, q be Element of CL; :: according to FILTER_0:def 6 :: thesis: ex b1 being Element of the carrier of CL st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of CL holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )

consider i being Element of IL such that
A2: f . i = p by ;
consider j being Element of IL such that
A3: f . j = q by ;
take r = f . (i => j); :: thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of CL holds
( not p "/\" b1 [= q or b1 [= r ) ) )

thus p "/\" r [= q by A2, A3, Th26; :: thesis: for b1 being Element of the carrier of CL holds
( not p "/\" b1 [= q or b1 [= r )

hereby :: thesis: verum
let r1 be Element of CL; :: thesis: ( p "/\" r1 [= q implies r1 [= r )
assume A4: p "/\" r1 [= q ; :: thesis: r1 [= r
ex k being Element of IL st f . k = r1 by ;
hence r1 [= r by A1, A2, A3, A4, Th27; :: thesis: verum
end;
end;
then reconsider CL = CL as implicative Lattice ;
reconsider f = f as Homomorphism of IL,CL ;
now :: thesis: for i, j being Element of IL holds (f . i) => (f . j) = f . (i => j)
let i, j be Element of IL; :: thesis: (f . i) => (f . j) = f . (i => j)
A5: now :: thesis: for r1 being Element of CL st (f . i) "/\" r1 [= f . j holds
r1 [= f . (i => j)
let r1 be Element of CL; :: thesis: ( (f . i) "/\" r1 [= f . j implies r1 [= f . (i => j) )
assume A6: (f . i) "/\" r1 [= f . j ; :: thesis: r1 [= f . (i => j)
ex k being Element of IL st f . k = r1 by ;
hence r1 [= f . (i => j) by A1, A6, Th27; :: thesis: verum
end;
(f . i) "/\" (f . (i => j)) [= f . j by Th26;
hence (f . i) => (f . j) = f . (i => j) by ; :: thesis: verum
end;
hence f preserves_implication ; :: thesis: verum