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 )

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

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

then (f . a1) "\/" (f . b1) = f . 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;then (f . a1) "\/" (f . b1) = f . 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