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 => b < a => b by Def2;
hence a "/\" (a => b) < b by Def4; :: thesis: verum