let L be 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)
( b "/\" c <= b & b "/\" c <= c & a <= a ) by YELLOW_0:23;
then ( a "\/" (b "/\" c) <= a "\/" b & a "\/" (b "/\" c) <= a "\/" c ) by YELLOW_3:3;
hence a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c) by YELLOW_0:23; :: thesis: verum