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