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