let L be distributive Lattice; :: thesis: for a, x1, x2 being Element of L holds a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2)
let a, x1, x2 be Element of L; :: thesis: a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2)
for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by LATTICES:def 11;
hence a "\/" (x1 "/\" x2) = (a "\/" x1) "/\" (a "\/" x2) by LATTICES:3; :: thesis: verum