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:1;
j "/\" (j => i) [= i by FILTER_0:def 7;
then A2: i "\/" (j "/\" (j => i)) [= i by A1, FILTER_0:1;
A3: (i "\/" j) "/\" (j => i) [= (i "\/" j) "/\" (i "\/" (j => i)) by LATTICES:5, LATTICES:9;
A4: j "/\" ((i "\/" j) => i) [= (i "\/" j) "/\" ((i "\/" j) => i) by LATTICES:5, LATTICES:9;
(i "\/" j) "/\" ((i "\/" j) => i) [= i by FILTER_0:def 7;
then j "/\" ((i "\/" j) => i) [= i by A4, LATTICES:7;
then A5: (i "\/" j) => i [= j => i by FILTER_0:def 7;
i "\/" (j "/\" (j => i)) = (i "\/" j) "/\" (i "\/" (j => i)) by LATTICES:11;
then (i "\/" j) "/\" (j => i) [= i by A2, A3, LATTICES:7;
then j => i [= (i "\/" j) => i by FILTER_0:def 7;
hence (i "\/" j) => i = j => i by A5, LATTICES:8; :: thesis: i => (i "/\" j) = i => j
A6: j "/\" i [= j by LATTICES:6;
i "/\" (i => (i "/\" j)) [= i "/\" j by FILTER_0:def 7;
then i "/\" (i => (i "/\" j)) [= j by A6, LATTICES:7;
then A7: i => (i "/\" j) [= i => j by FILTER_0:def 7;
A8: i "/\" i = i by LATTICES:2;
i "/\" (i => j) [= j by FILTER_0:def 7;
then A9: i "/\" (i "/\" (i => j)) [= i "/\" j by LATTICES:9;
i "/\" (i "/\" (i => j)) = (i "/\" i) "/\" (i => j) by LATTICES:def 7;
then i => j [= i => (i "/\" j) by A9, A8, FILTER_0:def 7;
hence i => (i "/\" j) = i => j by A7, LATTICES:8; :: thesis: verum