theorem :: FILTER_1:54

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