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)

A1: a <= a ;

c <= b "\/" c by YELLOW_0:22;

then A2: a "/\" c <= a "/\" (b "\/" c) by A1, YELLOW_3:2;

b <= b "\/" c by YELLOW_0:22;

then a "/\" b <= a "/\" (b "\/" c) by A1, YELLOW_3:2;

hence (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) by A2, YELLOW_5:9; :: thesis: verum

let a, b, c be Element of L; :: thesis: (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)

A1: a <= a ;

c <= b "\/" c by YELLOW_0:22;

then A2: a "/\" c <= a "/\" (b "\/" c) by A1, YELLOW_3:2;

b <= b "\/" c by YELLOW_0:22;

then a "/\" b <= a "/\" (b "\/" c) by A1, YELLOW_3:2;

hence (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c) by A2, YELLOW_5:9; :: thesis: verum