theorem Th24: :: NELSON_1:45

for L being Nelson_Algebra
for a, b being Element of L holds a => (b => a) = Top L