let L be Lattice; :: thesis: ( the L_join of L is_distributive_wrt the L_meet of L implies L is distributive )
assume A1: the L_join of L is_distributive_wrt the L_meet of L ; :: thesis: L is distributive
then A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by BINOP_1:12;
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 "/\" (c "\/" a)) "/\" (c "\/" b) by LATTICES:def 9
.= a "/\" ((c "\/" a) "/\" (c "\/" b)) by LATTICES:def 7
.= a "/\" ((a "/\" b) "\/" c) by A2
.= ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" c) by LATTICES:def 8
.= (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:12 ; :: thesis: verum