:: deftheorem defines satisfying_N1* NELSON_1:def 23 :
for L being non empty NelsonStr holds
( L is satisfying_N1* iff for a, b being Element of L holds a => (b => a) = Top L );