theorem Th18: :: NELSON_1:35
for L being Nelson_Algebra
for a, b, c being Element of L holds a => (b => c) = b => (a => c)