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