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)
( (i "/\" j) "/\" ((i "/\" j) => k) [= k & (j "/\" i) "/\" ((i "/\" j) => k) = j "/\" (i "/\" ((i "/\" j) => k)) & i "/\" j = j "/\" i ) by FILTER_0:def 8, LATTICES:def 7;
then i "/\" ((i "/\" j) => k) [= j => k by FILTER_0:def 8;
then A1: (i "/\" j) => k [= i => (j => k) by FILTER_0:def 8;
i "/\" (i => (j => k)) [= j => k by FILTER_0:def 8;
then ( j "/\" (i "/\" (i => (j => k))) [= j "/\" (j => k) & j "/\" (j => k) [= k & j "/\" i = i "/\" j & j "/\" (i "/\" (i => (j => k))) = (j "/\" i) "/\" (i => (j => k)) ) by FILTER_0:def 8, LATTICES:27, LATTICES:def 7;
then (i "/\" j) "/\" (i => (j => k)) [= k by LATTICES:25;
then i => (j => k) [= (i "/\" j) => k by FILTER_0:def 8;
hence (i "/\" j) => k = i => (j => k) by A1, LATTICES:26; :: thesis: verum