let I be I_Lattice; :: thesis: for i, j being Element of I holds
( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
let i, j be Element of I; :: thesis: ( (i "\/" j) => i = j => i & i => (i "/\" j) = i => j )
A1: i "\/" i = i by LATTICES:17;
j "/\" (j => i) [= i by FILTER_0:def 8;
then A2: i "\/" (j "/\" (j => i)) [= i by A1, FILTER_0:1;
A3: (i "\/" j) "/\" (j => i) [= (i "\/" j) "/\" (i "\/" (j => i)) by LATTICES:22, LATTICES:27;
A4: j "/\" ((i "\/" j) => i) [= (i "\/" j) "/\" ((i "\/" j) => i) by LATTICES:22, LATTICES:27;
(i "\/" j) "/\" ((i "\/" j) => i) [= i by FILTER_0:def 8;
then j "/\" ((i "\/" j) => i) [= i by A4, LATTICES:25;
then A5: (i "\/" j) => i [= j => i by FILTER_0:def 8;
i "\/" (j "/\" (j => i)) = (i "\/" j) "/\" (i "\/" (j => i)) by LATTICES:31;
then (i "\/" j) "/\" (j => i) [= i by A2, A3, LATTICES:25;
then j => i [= (i "\/" j) => i by FILTER_0:def 8;
hence (i "\/" j) => i = j => i by A5, LATTICES:26; :: thesis: i => (i "/\" j) = i => j
A6: j "/\" i [= j by LATTICES:23;
i "/\" (i => (i "/\" j)) [= i "/\" j by FILTER_0:def 8;
then i "/\" (i => (i "/\" j)) [= j by A6, LATTICES:25;
then A7: i => (i "/\" j) [= i => j by FILTER_0:def 8;
A8: i "/\" i = i by LATTICES:18;
i "/\" (i => j) [= j by FILTER_0:def 8;
then A9: i "/\" (i "/\" (i => j)) [= i "/\" j by LATTICES:27;
i "/\" (i "/\" (i => j)) = (i "/\" i) "/\" (i => j) by LATTICES:def 7;
then i => j [= i => (i "/\" j) by A9, A8, FILTER_0:def 8;
hence i => (i "/\" j) = i => j by A7, LATTICES:26; :: thesis: verum