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) = a ;
hence a =-> (Top L) = Top L by Def6; :: thesis: verum