theorem Th57: :: FILTER_1:57

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