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