let L be Nelson_Algebra; :: thesis: for a, b, c being Element of L holds a => (b => c) = b => (a => c)
let a, b, c be Element of L; :: thesis: a => (b => c) = b => (a => c)
a => (b => c) = (a "/\" b) => c by Lm3
.= b => (a => c) by Lm3 ;
hence a => (b => c) = b => (a => c) ; :: thesis: verum