theorem Th21: :: NELSON_1:41

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