theorem Th17: :: FILTER_1:17

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