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