theorem Th56: :: FILTER_1:56

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