for I being I_Lattice
for i, j, k being Element of I holds
( i => j [= i => (j "\/" k) & i => j [= (i "/\" k) => j & i => j [= i => (k "\/" j) & i => j [= (k "/\" i) => j )