let L be LATTICE; :: thesis: ( L is distributive implies for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) )
assume A1: L is distributive ; :: thesis: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
let a, b, c be Element of L; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c)
(a "\/" b) "/\" (a "\/" c) = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" c) by A1, WAYBEL_1:def 3
.= a "\/" ((a "\/" b) "/\" c) by LATTICE3:18
.= a "\/" ((c "/\" a) "\/" (c "/\" b)) by A1, WAYBEL_1:def 3
.= (a "\/" (c "/\" a)) "\/" (c "/\" b) by LATTICE3:14
.= a "\/" (c "/\" b) by LATTICE3:17 ;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) ; :: thesis: verum