let L be Lattice; :: thesis: ( the L_meet of L is_distributive_wrt the L_join of L implies L is distributive )
assume A1: the L_meet of L is_distributive_wrt the L_join of L ; :: thesis: L is distributive
let a be Element of L; :: according to LATTICES:def 11 :: thesis: for b₁, b₂ being Element of the carrier of L holds a "/\" (b₁ "\/" b₂) = (a "/\" b₁) "\/" (a "/\" b₂)
let b, c be Element of L; :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:24; :: thesis: verum