theorem :: NELSON_1:34

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