theorem :: NELSON_1:28

for L being Nelson_Algebra
for a being Element of L holds a =-> (Top L) = Top L