for L being Nelson_Algebra
for a, b being Element of L st a = Top L & a => b = Top L holds
b = Top L by Th23;