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