theorem Th31: :: NELSON_1:52

for L being Nelson_Algebra
for a, b, c being Element of L holds (a => b) => ((a => c) => (a => (b "/\" c))) = Top L