:: deftheorem Def12 defines satisfying_N11 NELSON_1:def 18 :
for L being non empty NelsonStr holds
( L is satisfying_N11 iff for a being Element of L holds - (! a) < a );