theorem Th25: :: NELSON_1:46

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