theorem :: NELSON_1:12

for L being Nelson_Algebra
for a, b being Element of L holds
( a <= b iff a =-> b = Top L ) by Def6;