theorem Th16ter: :: NELSON_1:29

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