let L1, L2 be Lattice; :: thesis: for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
let a1, b1 be Element of L1; :: thesis: for f being Homomorphism of L1,L2 st f is one-to-one holds
( a1 [= b1 iff f . a1 [= f . b1 )
let f be Homomorphism of L1,L2; :: thesis: ( f is one-to-one implies ( a1 [= b1 iff f . a1 [= f . b1 ) )
assume f is one-to-one ; :: thesis: ( a1 [= b1 iff f . a1 [= f . b1 )
then A1: f is one-to-one ;
reconsider f = f as Function of the carrier of L1,the carrier of L2 ;
( f . a1 [= f . b1 implies a1 [= b1 )

proof

assume f . a1 [= f . b1 ; :: thesis: a1 [= b1
then (f . a1) "\/" (f . b1) = f . b1 by LATTICES:def 3;
then f . (a1 "\/" b1) = f . b1 by Def1;
hence a1 "\/" b1 = b1 by A1, FUNCT_2:25; :: according to LATTICES:def 3 :: thesis: verum

end;

hence ( a1 [= b1 iff f . a1 [= f . b1 ) by Th7; :: thesis: verum