let L2 be Lattice; :: thesis: for DL being distributive Lattice
for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let DL be distributive Lattice; :: thesis: for f being Homomorphism of DL,L2 st f is onto holds
L2 is distributive
let f be Homomorphism of DL,L2; :: thesis: ( f is onto implies L2 is distributive )
assume A1: f is onto ; :: thesis: L2 is distributive
thus L2 is distributive :: thesis: verum

proof

let a, b, c be Element of L2; :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
consider a9 being Element of DL such that
A2: f . a9 = a by A1, Th6;
consider c9 being Element of DL such that
A3: f . c9 = c by A1, Th6;
consider b9 being Element of DL such that
A4: f . b9 = b by A1, Th6;
thus a "/\" (b "\/" c) = a "/\" (f . (b9 "\/" c9)) by A4, A3, D1
.= f . (a9 "/\" (b9 "\/" c9)) by A2, D2
.= f . ((a9 "/\" b9) "\/" (a9 "/\" c9)) by LATTICES:def 11
.= (f . (a9 "/\" b9)) "\/" (f . (a9 "/\" c9)) by D1
.= (a "/\" b) "\/" (f . (a9 "/\" c9)) by A2, A4, D2
.= (a "/\" b) "\/" (a "/\" c) by A2, A3, D2 ; :: thesis: verum

end;