:: deftheorem Def14 defines satisfying_N13 NELSON_1:def 20 :
for L being non empty NelsonStr holds
( L is satisfying_N13 iff for a being Element of L holds ! a = a => (- (Top L)) );