let L be D_Lattice; :: 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)
for a, b, c being Element of L holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by Def11;
hence a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by Th1; :: thesis: verum