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