let L be LATTICE; :: thesis: for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)
let a, b, c be Element of L; :: thesis: (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)
( b <= b "\/" c & c <= b "\/" c & a <= a ) by YELLOW_0:22;
then ( a "/\" b <= a "/\" (b "\/" c) & a "/\" c <= a "/\" (b "\/" c) ) by YELLOW_3:2;
hence (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) by YELLOW_5:9; :: thesis: verum