:: deftheorem Def10 defines satisfying_N9 NELSON_1:def 16 :
for L being non empty NelsonStr holds
( L is satisfying_N9 iff for a, b being Element of L holds - (a => b) < a "/\" (- b) );