let L be Nelson_Algebra; :: thesis: for a being Element of L holds a => (Top L) = Top L
let a be Element of L; :: thesis: a => (Top L) = Top L
a <= Top L by LATTICES:4, LATTICES:19;
then a < Top L by Th5;
hence a => (Top L) = Top L ; :: thesis: verum