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