let I be I_Lattice; :: thesis: for i, j, k being Element of I holds
( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
let i, j, k be Element of I; :: thesis: ( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )
A1: i "/\" (i => j) [= j by FILTER_0:def 7;
(i "/\" k) "/\" (i => j) [= i "/\" (i => j) by LATTICES:6, LATTICES:9;
then A2: (i "/\" k) "/\" (i => j) [= j by A1, LATTICES:7;
j [= j "\/" k by LATTICES:5;
then i "/\" (i => j) [= j "\/" k by A1, LATTICES:7;
hence ( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j ) by A2, FILTER_0:def 7; :: thesis: verum