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 A1: f is one-to-one ; :: thesis: ( a1 [= b1 iff f . a1 [= f . b1 )
reconsider f = f as Function of L1,L2 ;
( f . a1 [= f . b1 implies a1 [= b1 )

proof

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

end;

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