let L1, L2 be Lattice; :: thesis: for a1, b1 being Element of L1
for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
let a1, b1 be Element of L1; :: thesis: for f being Homomorphism of L1,L2 st a1 [= b1 holds
f . a1 [= f . b1
let f be Homomorphism of L1,L2; :: thesis: ( a1 [= b1 implies f . a1 [= f . b1 )
assume A1: a1 [= b1 ; :: thesis: f . a1 [= f . b1
(f . a1) "\/" (f . b1) = f . (a1 "\/" b1) by Def1
.= f . b1 by A1, LATTICES:def 3 ;
hence f . a1 [= f . b1 by LATTICES:def 3; :: thesis: verum