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

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;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