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)

A1: a <= a ;

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

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

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

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

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

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

A1: a <= a ;

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

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

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

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

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