theorem :: NELSON_1:27
for L being Nelson_Algebra
for a, b being Element of L st a =-> b = Top L & b =-> a = Top L holds
a = b