let L be LATTICE; :: thesis: for a, b, c being Element of L st a <= c holds

a "\/" (b "/\" c) <= (a "\/" b) "/\" c

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

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

A2: a <= a ;

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

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

assume a <= c ; :: thesis: a "\/" (b "/\" c) <= (a "\/" b) "/\" c

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

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

a "\/" (b "/\" c) <= (a "\/" b) "/\" c

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

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

A2: a <= a ;

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

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

assume a <= c ; :: thesis: a "\/" (b "/\" c) <= (a "\/" b) "/\" c

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

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