let L be Lattice; :: thesis: ( L is distributive implies L is modular )
assume A1: L is distributive ; :: thesis: L is modular
let a, b, c be Element of L; :: according to LATTICES:def 12 :: thesis: ( a [= c implies a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume a "\/" c = c ; :: according to LATTICES:def 3 :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
hence a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, Th9; :: thesis: verum